English
Let F be a possibly infinite family of compact convex sets in a finite-dimensional space E. If every subfamily of size d+1 has nonempty intersection, then the intersection of all sets in F is nonempty.
Русский
Пусть F — возможно бесконечное семейство компактных выпуклых множеств в конечномерном пространстве E. Если любая подподсемейство из F размера d+1 имеет непустое пересечение, то пересечение всей F непусто.
LaTeX
$$$\\displaystyle\\text{Let } F = \\{F_i\\}_{i\\in I} \\text{ be a (possibly infinite) family of compact convex subsets of } E. \\\\ \\text{If every subfamily with } |J| = d+1 \\ has \\\\ \\bigcap_{i\\in J} F_i \\neq \\emptyset, \\text{ then } \\bigcap_{i\\in I} F_i \\neq \\emptyset.$$$
Lean4
/-- **Helly's theorem** for families of compact convex sets in its classical form.
If `F` is a (possibly infinite) family of more than `d + 1` compact convex sets in a vector space of
finite dimension `d`, and any `d + 1` sets of `F` intersect nontrivially,
then all sets of `F` intersect nontrivially. -/
theorem helly_theorem_compact [TopologicalSpace E] [T2Space E] {F : ι → Set E} (h_card : finrank 𝕜 E + 1 ≤ ENat.card ι)
(h_convex : ∀ i, Convex 𝕜 (F i)) (h_compact : ∀ i, IsCompact (F i))
(h_inter : ∀ I : Finset ι, #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) : (⋂ i, F i).Nonempty :=
by
apply helly_theorem_compact' h_convex h_compact
intro I hI_card
have hJ : ∃ J : Finset ι, I ⊆ J ∧ #J = finrank 𝕜 E + 1 :=
by
by_cases h : Infinite ι
· exact Infinite.exists_superset_card_eq _ _ hI_card
· have : Finite ι := Finite.of_not_infinite h
have : Fintype ι := Fintype.ofFinite ι
apply exists_superset_card_eq hI_card
simp only [ENat.card_eq_coe_fintype_card] at h_card
rwa [← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at h_card
obtain ⟨J, hJ_ss, hJ_card⟩ := hJ
apply Set.Nonempty.mono <| biInter_mono hJ_ss (by intro _ _; rfl)
exact h_inter J hJ_card
