English
If S and T are nonempty subsets, the same equality as above holds: convHull(S ∪ T) = convexJoin(convHull S, convHull 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
theorem convexHull_union (hs : s.Nonempty) (ht : t.Nonempty) :
convexHull 𝕜 (s ∪ t) = convexJoin 𝕜 (convexHull 𝕜 s) (convexHull 𝕜 t) :=
by
rw [← convexHull_convexHull_union_left, ← convexHull_convexHull_union_right]
exact (convex_convexHull 𝕜 s).convexHull_union (convex_convexHull 𝕜 t) hs.convexHull ht.convexHull
