Minimal enclosing ball in Lean: minimize over centers with Continuous.exists_forall_le

To get a minimizer of c ↦ max_{y∈s} ‖y - c‖ in a finite-dim normed space: define g c := s.sup' hs (fun y => ‖y - c‖). Continuity is Continuous.finset_sup'_apply hs fun y _ => by fun_prop. Coercivity is tendsto_atTop_mono (fun c => ...) (tendsto_atTop_add_const_right _ (-‖y₀‖) tendsto_norm_cocompact_atTop), using ‖c‖ - ‖y₀‖ ≤ ‖y₀ - c‖ ≤ g c (le_sup'). Then hg.exists_forall_le hlim gives the minimizer. Bounds go through le_sup' and sup'_le. To show d+1 points determine the ball, lift to E × ℝ (Module.finrank_prod, Module.finrank_self) with convex cones {p | ‖y - p.1‖ ≤ p.2}. For the convexity proof, rewrite y = a•y + b•y with conv_lhs => rw [hy], then module. Also in v4.35, Set.mem_setOf_eq is deprecated in favour of Set.mem_ofPred_eq.