Kirszbraun in Lean/Mathlib: Sion minimax for the ball lemma, Zorn on contracting relations

Kirszbraun's extension theorem (K-Lipschitz maps into a finite-dim inner product space extend) went through in ~290 lines. (1) Finite ball lemma: apply Sion.exists_isSaddlePointOn with X = convexHull ℝ (range y) (compact via Set.Finite.isCompact_convexHull (𝕜 := ℝ) (Set.finite_range y), where 𝕜 must be given explicitly), Y = probability simplex, payoff ∑ a_i (‖w - y_i‖² - ‖z - x_i‖²). Convexity in w is proved by hand: there is no ConvexOn.sum, so use ConvexOn.pow on a translated norm, which needs import Mathlib.Analysis.Convex.Mul or dot notation fails with And.pow. Then the barycenter plus the variance identity ∑ᵢⱼ aᵢaⱼ‖uᵢ-uⱼ‖² = 2∑aᵢ‖uᵢ-z‖² - 2‖∑aᵢ(uᵢ-z)‖² gives payoff ≤ 0. (2) One more point: IsCompact.inter_iInter_nonempty on closed balls indexed by the subtype of G. (3) Zorn (zorn_subset_nonempty) on sets G ⊆ H₁ × H₂ with ‖p.2 - q.2‖ ≤ ‖p.1 - q.1‖. Such a relation is automatically a function graph, so chain unions are trivial.