English
Let ι be an index set and 𝕜 a field; E is finite-dimensional. If F : Set of convex compact subsets of E satisfies that the index-encard permits more than d+1 elements and any d+1 of them intersect, then the intersection of all is nonempty.
Русский
Пусть ι множество индексов, 𝕜 полe, E конечномерное. Пусть F — множество компактных выпуклых подмножеств пространства E. Если число элементов больше d+1 в экватк, и любые d+1 из них пересекаются, то всё пересечение непусто.
LaTeX
$$$\\displaystyle\\text{Let } F: ι \\to \\mathcal{P}(E) \\text{ with each } F(i) \\text{ compact convex and } |F| \\ge d+1. \\\\ \\text{If every subfamily of size } d+1 \\ has nonempty intersection, then } \\bigcap_{i\\in ι} F(i) \\neq \\emptyset.$$$
Lean4
/-- **Helly's theorem** for sets of compact convex sets in its classical version.
If `F` is a (possibly infinite) set of more than `d + 1` compact convex sets in a vector space of
finite dimension `d`, and any `d + 1` sets from `F` intersect nontrivially,
then all sets from `F` intersect nontrivially. -/
theorem helly_theorem_set_compact [TopologicalSpace E] [T2Space E] {F : Set (Set E)}
(h_card : finrank 𝕜 E + 1 ≤ F.encard) (h_convex : ∀ X ∈ F, Convex 𝕜 X) (h_compact : ∀ X ∈ F, IsCompact X)
(h_inter : ∀ G : Finset (Set E), (G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ G : Set E).Nonempty) :
(⋂₀ (F : Set (Set E))).Nonempty :=
by
apply helly_theorem_set_compact' h_convex h_compact
intro I hI_ss hI_card
obtain ⟨J, _, hJ_ss, hJ_card⟩ :=
exists_superset_subset_encard_eq hI_ss (hkt := h_card)
(by simpa only [encard_coe_eq_coe_finsetCard, ← ENat.coe_one, ← ENat.coe_add, Nat.cast_le])
apply Set.Nonempty.mono <| sInter_mono (by simpa [hI_ss])
have hJ_fin : Fintype J := Finite.fintype <| finite_of_encard_eq_coe hJ_card
let J' := J.toFinset
rw [← coe_toFinset J]
apply h_inter J'
· simpa [J']
· rwa [encard_eq_coe_toFinset_card J, ← ENat.coe_one, ← ENat.coe_add, Nat.cast_inj] at hJ_card
