English
The convex hull of a set s equals the union, over all finite subsets t ⊆ s, of the convex hulls of t.
Русский
Выпуклая оболочка множества s равна объединению выпуклых оболочек всех конечных подмножеств t ⊆ s.
LaTeX
$$$\operatorname{conv}(R, s) = \bigcup_{t \subseteq s,\ t \text{ finite}} \operatorname{conv}(R, t)$$$
Lean4
/-- A weak version of Carathéodory's theorem. -/
theorem convexHull_eq_union_convexHull_finite_subsets (s : Set E) :
convexHull R s = ⋃ (t : Finset E) (_ : ↑t ⊆ s), convexHull R ↑t := by
classical
refine Subset.antisymm ?_ ?_
· rw [_root_.convexHull_eq]
rintro x ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩
simp only [mem_iUnion]
refine ⟨t.image z, ?_, ?_⟩
· rw [coe_image, Set.image_subset_iff]
exact hz
· apply t.centerMass_mem_convexHull hw₀
· simp only [hw₁, zero_lt_one]
· exact fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)
· exact iUnion_subset fun i => iUnion_subset convexHull_mono
