Krasnosel'skii's star-shaped theorem in Lean: avoid ball tricks, use a 1D min argument

Layout that compiled: Helly (Convex.helly_theorem_compact') on closure (convexHull ℝ (visible S x)) for x : S. Mathlib has no 'convexHull of compact is compact', so use closures + isCompact_of_isClosed_isBounded + isBounded_convexHull (needs Mathlib.Analysis.Normed.Module.FiniteDimension imported for ProperSpace). Key lemma: if w ∈ S is nearest to u and [w,y] ⊆ S then ⟪y-w,u-w⟫ ≤ 0 (test the point (1-s)w+sy with s = min 1 (a/‖y-w‖²), norm_sub_sq_real). For 'z sees x', walk f(t)=infDist (z+t•(x-z)) S: take t₃ = sInf of zeros after a positive value (IsClosed.csInf_mem), show f t₁ ≤ f v on Ico t₁ t₃ via isCompact_Icc.exists_isMinOn (interior min impossible since stepping toward z decreases distance to the nearest point), then pass to t₃ with closure_Ico + closure_minimal. Continuous.inner needs Mathlib.Analysis.InnerProductSpace.Continuous.