English
Let F be a finite family of convex subsets of E with d = dim𝕜(E). If |F| ≥ d + 1 and every subfamily of size d + 1 has nonempty intersection, then the intersection of all sets in F is nonempty.
Русский
Пусть F — конечное семейство выпуклых подмножеств пространства E. Пусть d = dim𝕜(E). Если |F| ≥ d + 1 и пересечение любой подподсемейства размера d + 1 непусто, то пересечение всей F непусто.
LaTeX
$$$\\displaystyle\\text{Let } F = \\{F_i\\}_{i\\in s} \\text{ be a finite family of convex subsets of } E.\\\\ \\text{If } |s| \\ge \\dim(E) + 1 \\text{ and every subfamily of size } d+1 \\text{ has nonempty intersection, then } \\bigcap_{i\\in s} F_i \\neq \\emptyset.$$$
Lean4
/-- **Helly's theorem** for finite sets of convex sets in its classical form.
If `F` is a finite set of convex sets in a vector space of finite dimension `d`, with `n ≥ d + 1`,
and any `d + 1` sets from `F` intersect nontrivially,
then all sets from `F` intersect nontrivially. -/
theorem helly_theorem_set {F : Finset (Set E)} (h_card : finrank 𝕜 E + 1 ≤ #F) (h_convex : ∀ X ∈ F, Convex 𝕜 X)
(h_inter : ∀ G : Finset (Set E), G ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ G : Set E).Nonempty) :
(⋂₀ (F : Set (Set E))).Nonempty := by
apply helly_theorem_set' h_convex
intro I hI_ss hI_card
obtain ⟨J, _, hJ_ss, hJ_card⟩ := exists_subsuperset_card_eq hI_ss hI_card h_card
have : ⋂₀ (J : Set (Set E)) ⊆ ⋂₀ I := sInter_mono (by simpa [hI_ss])
apply Set.Nonempty.mono this
exact h_inter J hJ_ss (by cutsat)
