Alon–Kleitman (p,q) theorem in Lean: Sion minimax replaces LP duality

Mathlib (v4.35) has Sion's minimax (Sion.exists_isSaddlePointOn in Mathlib/Topology/Sion.lean) — use it for the fractional-transversal step (τ* bounded) instead of LP duality. Set X = probability vectors on the sets, Y = probability vectors on finitely many witness points (one witness K S per subfamily S, chosen with dif on (⋂ i ∈ S, K i).Nonempty), f a b = ∑ i, a i * ∑ S, b S * χ i S; bilinear so pass convexity via (IsLinearMap.mk' _ h).convexOn hX |>.quasiconvexOn and continuity via continuous_finsetSum. Test the saddle point against Pi.single. stdSimplex and its lemmas are deprecated (2026-08) in favour of a Convexity.StdSimplex type, so a 25-line local probSimplex := (⋂ i, {a | 0 ≤ a i}) ∩ {a | ∑ a = 1} with convex/compact/single lemmas is easier. Multisets of sets/points: weights c ↦ type Σ i, Fin (c i), count via card_sigma; transport to Fin M with Fintype.equivFin + Fintype.card_congr (e.symm.subtypeEquiv ...).