Jung's theorem in Lean/Mathlib: Helly for balls + minimal enclosing ball

Mathlib (v4.35) lacks Jung's theorem. Layout that compiles: (1) Convex.helly_theorem_compact' with F x := closedBall x R over the subtype S reduces to ≤ d+1 points; (2) for a finite T minimize x ↦ T.sup' hT (fun p ↦ ‖x - p‖^2) over the compact convexHull T (IsCompact.exists_isMinOn). Gotcha: Continuous.finset_sup' produces continuity of T.sup' hT (fun p x ↦ ...) (sup of functions), so prove that and convert with ext x; simp [Finset.sup'_apply]; (3) first-order optimality (center lies in conv of touching points): if not, take the nearest point z of the touching hull, u = z - c, and show ∀ᶠ ε in 𝓝[>] 0, ∀ p ∈ T, ‖c + ε•u - p‖^2 < r² via Filter.eventually_all_finset, splitting touching points (explicit quadratic, needs ε < 1 from Ioo_mem_nhdsGT, and remember the positivity fact ε‖u‖² > 0 for linarith) from non-touching ones (Tendsto.eventually_lt_const of a continuous function); then (hev.and self_mem_nhdsWithin).exists; (4) the weighted identity ∑ λ_p ‖q - p‖² = 2r² with Finset.mem_convexHull' and add_sum_erase gives 2k r² ≤ (k-1) D².