English
Carathéodory's convexity: the convex hull of s equals the union, over all finite affinely independent subsets t of s, of the convex hull of t.
Русский
Свод Каретадеодори: выпуклая оболочка множества s равна объединению выпуклых оболочек по всем конечным аффинно независимым подмножествам t ⊆ s.
LaTeX
$$$\\operatorname{convexHull}\\,\\mathbb{K}\\,s = \\bigcup_{t\\subseteq s,\\ AffineIndependent( t )}\\operatorname{convexHull}\\,\\mathbb{K}\\,t$$$
Lean4
/-- **Carathéodory's convexity theorem** -/
theorem convexHull_eq_union :
convexHull 𝕜 s = ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 ((↑) : t → E)), convexHull 𝕜 ↑t :=
by
apply Set.Subset.antisymm
· intro x hx
simp only [exists_prop, Set.mem_iUnion]
exact
⟨Caratheodory.minCardFinsetOfMemConvexHull hx, Caratheodory.minCardFinsetOfMemConvexHull_subseteq hx,
Caratheodory.affineIndependent_minCardFinsetOfMemConvexHull hx,
Caratheodory.mem_minCardFinsetOfMemConvexHull hx⟩
· iterate 3 convert Set.iUnion_subset _; intro
exact convexHull_mono ‹_›
