English
For any point x and any set S with S nonempty, the convex hull of insert x S equals the convexJoin of {x} with the convex hull of S.
Русский
Для любой точки x и множества S с S не пустым, выпуклая оболочка вставки x в S равна выпуклому объединению {x} и выпуклой оболочки S.
LaTeX
$$$\\operatorname{convexHull}_{\\mathbb{K}}(\\operatorname{insert}_{\\mathbb{K}}(x,S))=\\operatorname{convexJoin}_{\\mathbb{K}}(\\{x\\},\\operatorname{convexHull}_{\\mathbb{K}}(S)).$$$
Lean4
theorem convexHull_insert (hs : s.Nonempty) : convexHull 𝕜 (insert x s) = convexJoin 𝕜 { x } (convexHull 𝕜 s) := by
rw [insert_eq, convexHull_union (singleton_nonempty _) hs, convexHull_singleton]
