English
Let F be a (possibly infinite) set of compact convex sets. If any d+1 members of F have nonempty intersection, then the whole family has nonempty intersection.
Русский
Пусть F — множество допустимых (возможно бесконечного) компактных выпуклых множеств. Если любые d+1 элементов F имеют непустое пересечение, то пересечение всей F непусто.
LaTeX
$$$\\displaystyle\\text{Let } F \\subseteq \\mathcal{P}(E) \\text{ be a (possibly infinite) set of compact convex sets. } \\\\ \\text{If for every finite } G\\subseteq F \\\\ |G| \\le d+1 \\Rightarrow \\bigcap_{X\\in G} X \\neq \\emptyset, \\\\ \\bigcap_{X\\in F} X \\neq \\emptyset.$$$
Lean4
/-- **Helly's theorem** for sets of compact convex sets.
If `F` is a set of compact 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_compact' [TopologicalSpace E] [T2Space E] {F : Set (Set E)} (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
classical -- for DecidableEq, required for the family version
rw [show ⋂₀ F = ⋂ X : F, (X : Set E) by ext; simp]
refine
helly_theorem_compact' (F := fun x : F ↦ x.val) (fun X ↦ h_convex X (by simp)) (fun X ↦ h_compact X (by simp)) ?_
intro G _
let G' : Finset (Set E) := image Subtype.val G
rw [show ⋂ i ∈ G, ↑i = ⋂₀ (G' : Set (Set E)) by simp [G']]
apply h_inter G'
· simp [G']
· apply le_trans card_image_le
assumption
