English
Let F be a finite family of convex subsets of a finite-dimensional vector space E over a field 𝕜. If every subfamily of F with at most d + 1 members has nonempty intersection, then the intersection of all members of F is nonempty. Here d = dim𝕜(E).
Русский
Пусть F — конечное семейство выпуклых подмножеств в векторном пространстве E над полем 𝕜 и что размерность пространства равна d = dim𝕜(E). Если любая подподмножество из F размером не более d + 1 имеет непустое пересечение, то пересечение всех множест F также непусто.
LaTeX
$$$\\displaystyle\\text{Let } F = \\{F_i\\}_{i\\in s} \\text{ be a finite family of convex subsets of a finite-dimensional vector space } E. \\\\ \\text{If every subfamily of size } |I| \\le \\dim(E) + 1 \\text{ satisfies } \\bigcap_{i\\in I} F_i \\neq \\emptyset, \\\\ \\text{then } \\bigcap_{i\\in s} F_i \\neq \\emptyset.}$$$
Lean4
/-- **Helly's theorem** for finite families of convex sets.
If `F` is a finite family of 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' {F : ι → Set E} {s : Finset ι} (h_convex : ∀ i ∈ s, Convex 𝕜 (F i))
(h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) : (⋂ i ∈ s, F i).Nonempty := by
classical
obtain h_card | h_card := lt_or_ge (#s) (finrank 𝕜 E + 1)
· exact helly_theorem_corner (le_of_lt h_card) h_inter
generalize hn : #s = n
rw [hn] at h_card
induction n, h_card using Nat.le_induction generalizing ι with
| base => exact helly_theorem_corner (le_of_eq hn) h_inter
| succ k h_card
hk =>
let a (i : s) : E :=
Set.Nonempty.some (s := ⋂ j ∈ s.erase i, F j) <|
by
apply hk (s := s.erase i)
· exact fun i hi ↦ h_convex i (mem_of_mem_erase hi)
· intro J hJ_ss hJ_card
exact h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card
· simp only [coe_mem, card_erase_of_mem];
cutsat
/- This family of vectors is not affine independent because the number of them exceeds the
dimension of the space. -/
have h_ind : ¬AffineIndependent 𝕜 a :=
by
rw [← finrank_vectorSpan_le_iff_not_affineIndependent 𝕜 a (n := (k - 1))]
· exact (Submodule.finrank_le (vectorSpan 𝕜 (range a))).trans (Nat.le_pred_of_lt h_card)
· simp only [card_coe];
cutsat
/- Use `radon_partition` to conclude there is a subset `I` of `s` and a point `p : E` which
lies in the convex hull of either `a '' I` or `a '' Iᶜ`. We claim that `p ∈ ⋂ i ∈ s, F i`. -/
obtain ⟨I, p, hp_I, hp_Ic⟩ := radon_partition h_ind
use p
apply mem_biInter
intro i hi
let i : s :=
⟨i, hi⟩
/- It suffices to show that for any subcollection `J` of `s` containing `i`, the convex
hull of `a '' (s \ J)` is contained in `F i`. -/
suffices ∀ J : Set s, (i ∈ J) → (convexHull 𝕜) (a '' Jᶜ) ⊆ F i
by
by_cases h : i ∈ I
· exact this I h hp_Ic
· apply this Iᶜ h;
rwa [compl_compl]
/- Given any subcollection `J` of `ι` containing `i`, because `F i` is convex, we need only
show that `a j ∈ F i` for each `j ∈ s \ J`. -/
intro J hi
rw [convexHull_subset_iff (h_convex i.1 i.2)]
rintro v ⟨j, hj, hj_v⟩
rw [← hj_v]
/- Since `j ∈ Jᶜ` and `i ∈ J`, we conclude that `i ≠ j`, and hence by the definition of `a`:
`a j ∈ ⋂ F '' (Set.univ \ {j}) ⊆ F i`. -/
apply mem_of_subset_of_mem (s₁ := ⋂ k ∈ (s.erase j), F k)
· apply biInter_subset_of_mem
simp only [erase_val]
suffices h : i.val ∈ s.erase j by assumption
simp only [mem_erase]
constructor
· exact fun h' ↦ hj ((show i = j from SetCoe.ext h') ▸ hi)
· assumption
· apply Nonempty.some_mem
