English
Let F be a set of convex compact sets. If for every finite G ⊆ F with |G| ≤ d+1 we have ⋂₀ G ≠ ∅, then ⋂₀ F ≠ ∅.
Русский
Пусть F — множество выпуклых компактных множеств. Если для каждого конечного подмножества G ⊆ F с |G| ≤ d+1 пересечение ⋂ G ненулево, то ⋂ F ненулево.
LaTeX
$$$\\displaystyle\\text{If } F \\subseteq \\mathcal{P}(E) \\text{ is a set of compact convex sets and } \\forall G \\subseteq F, |G| \\le d+1, \\bigcap G \\neq \\emptyset, \\text{ then } \\bigcap_{X\\in F} X \\neq \\emptyset.$$$
Lean4
theorem segment_subset_iff : [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⟩
