English
Let F be a finite collection of convex subsets of E. If for every subcollection G ⊆ F, with card(G) ≤ d + 1, the intersection ⋂G is nonempty, then ⋂F is nonempty.
Русский
Пусть F — конечная совокупность выпуклых подмножеств пространства E. Если для каждого конечного подмножества G ⊆ F с cardinality не более d + 1 пересечение ⋂G непусто, то пересечение всей F непусто.
LaTeX
$$$\\displaystyle\\text{Let } F \\subseteq \\mathcal{P}(E) \\text{ be finite with convex } X\\text{ for } X\\in F. \\\\ \\text{If } \\bigcap_{X\\in G} X \\neq \\emptyset \\text{ for all } G \\subseteq F \\text{ with } |G| \\le \\dim(E)+1, \\\\ \\text{then } \\bigcap_{X\\in F} X \\neq \\emptyset.$$$
Lean4
/-- **Helly's theorem** for finite sets of convex sets.
If `F` is a finite set of convex sets in a vector space of finite dimension `d`, and any `k ≤ d + 1`
sets from `F` intersect nontrivially, then all sets from `F` intersect nontrivially. -/
theorem helly_theorem_set' {F : Finset (Set E)} (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
classical -- for DecidableEq, required for the family version
rw [show ⋂₀ F = ⋂ X ∈ F, (X : Set E) by ext; simp]
apply helly_theorem' h_convex
intro G hG_ss hG_card
rw [show ⋂ X ∈ G, X = ⋂₀ G by ext; simp]
exact h_inter G hG_ss hG_card
