English
Let F = {F_i} be a family of convex sets in a finite-dimensional vector space E. If |F| ≥ d + 1 and every subfamily of size d + 1 has nonempty intersection, then the intersection of all F_i is nonempty.
Русский
Пусть F = {F_i} — семейство выпуклых множеств в конечномерном пространстве E. Если |F| ≥ d + 1 и любая подподмножество размера d + 1 имеет непустое пересечение, то пересечение всех F_i непусто.
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 } \\dim(E) + 1 \\text{ has nonempty intersection, then } \\bigcap_{i\\in s} F_i \\neq \\emptyset.$$$
Lean4
/-- **Helly's theorem** for finite families of convex sets in its classical form.
If `F` is a family of `n` convex sets in a vector space of finite dimension `d`, with `n ≥ d + 1`,
and any `d + 1` sets of `F` intersect nontrivially, then all sets of `F` intersect nontrivially. -/
theorem helly_theorem {F : ι → Set E} {s : Finset ι} (h_card : finrank 𝕜 E + 1 ≤ #s)
(h_convex : ∀ i ∈ s, Convex 𝕜 (F i)) (h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
(⋂ i ∈ s, F i).Nonempty := by
apply helly_theorem' h_convex
intro I hI_ss hI_card
obtain ⟨J, hI_ss_J, hJ_ss, hJ_card⟩ := exists_subsuperset_card_eq hI_ss hI_card h_card
apply Set.Nonempty.mono <| biInter_mono hI_ss_J (fun _ _ ↦ Set.Subset.rfl)
exact h_inter J hJ_ss hJ_card
