English
If S and T are subsets with S and T nonempty, then the convex hull of S ∪ T equals the convexJoin of the convex hulls of S and T:
Русский
Пусть S и T не пусты. Выпуклая оболочка S ∪ T равна выпуклому объединению выпуклых оболочек S и T.
LaTeX
$$$\\operatorname{convexHull}_{\\mathbb{K}}(S \\cup T)=\\operatorname{convexJoin}_{\\mathbb{K}}(\\operatorname{convexHull}_{\\mathbb{K}}(S),\\operatorname{convexHull}_{\\mathbb{K}}(T)).$$$
Lean4
protected theorem convexHull_union (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hs₀ : s.Nonempty) (ht₀ : t.Nonempty) :
convexHull 𝕜 (s ∪ t) = convexJoin 𝕜 s t :=
(convexHull_min (union_subset (subset_convexJoin_left ht₀) <| subset_convexJoin_right hs₀) <|
hs.convexJoin ht).antisymm <|
convexJoin_subset_convexHull _ _
