English
Let 𝕜 be a field and E a finite-dimensional vector space. If F is a family of compact convex subsets of E and any k ≤ d + 1 of them have a nonempty intersection, then the whole intersection ⋂ F is nonempty.
Русский
Пусть 𝕜 — поле, E — конечномерное векторное пространство. Пусть F — семейство компактных выпуклых подмножеств пространства E; если любой набор из k ≤ d+1 элементов имеет непустое пересечение, то пересечение всей F непусто.
LaTeX
$$$\\displaystyle\\text{Let } F = \\{F_i\\}_{i\\in I} \\text{ be a family of compact convex subsets of } E. \\\\ \\text{If } k \\le \\dim(E)+1 \text{ and every subfamily of size } k \\ has nonempty intersection, \\\\ \\bigcap_{i\\in I} F_i \\neq \\emptyset.$$$
Lean4
/-- **Helly's theorem** for families of compact convex sets.
If `F` is a family of compact convex sets in a vector space of finite dimension `d`, and any
`k ≤ 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_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
classical
/- If `ι` is empty the statement is trivial. -/
rcases isEmpty_or_nonempty ι with _ | h_nonempty
·
simp only [iInter_of_empty, Set.univ_nonempty]
/- By the finite version of theorem, every finite subfamily has an intersection. -/
have h_fin (I : Finset ι) : (⋂ i ∈ I, F i).Nonempty :=
by
apply helly_theorem' (s := I) (𝕜 := 𝕜) (by simp [h_convex])
exact fun J _ hJ_card ↦ h_inter J hJ_card
have i0 : ι := Nonempty.some h_nonempty
rw [show ⋂ i, F i = (F i0) ∩ ⋂ i, F i by simp [iInter_subset]]
apply IsCompact.inter_iInter_nonempty
· exact h_compact i0
· intro i
exact (h_compact i).isClosed
· intro I
simpa using h_fin ({ i0 } ∪ I)
