English
Let 𝕜 be a field and E a finite-dimensional vector space. If F is a set of compact convex sets and for every finite subcollection G ⊆ F with |G| = d+1 we have ⋂ G ≠ ∅, then ⋂ F ≠ ∅.
Русский
Пусть 𝕜 — поле, E — конечномерное векторное пространство. Пусть F — множество компактных выпуклых множеств. Если для каждого конечного подмножества G ⊆ F размера d+1 пересечение ⋂ G непусто, то пересечение всей F непусто.
LaTeX
$$$\\displaystyle\\text{Let } F \\subseteq \\mathcal{P}(E) \\text{ be a set of finite collections of compact convex sets. If } \\forall G \\subseteq F, |G| = d+1, \\bigcap_{X\\in G} X \\neq \\emptyset, \\text{ then } \\bigcap_{X\\in F} X \\neq \\emptyset.$$$
Lean4
theorem openSegment_subset_iff : openSegment 𝕜 x y ⊆ s ↔ ∀ a b : 𝕜, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s :=
⟨fun H a b ha hb hab => H ⟨a, b, ha, hb, hab, rfl⟩, fun H _ ⟨a, b, ha, hb, hab, hz⟩ => hz ▸ H a b ha hb hab⟩
