English
The join of two line segments equals the convex hull of their four endpoints: for a,b,c,d in E, convexJoin(seg(a,b), seg(c,d)) = convHull{a,b,c,d}.
Русский
Соединение двух отрезков равно выпуклой оболочке четырех концов: convexJoin(seg(a,b), seg(c,d)) = convHull{a,b,c,d}.
LaTeX
$$$\\operatorname{convexJoin}_{\\mathbb{K}}(\\operatorname{segment}_{\\mathbb{K}}(a,b),\\operatorname{segment}_{\\mathbb{K}}(c,d))=\\operatorname{convexHull}_{\\mathbb{K}}\\{a,b,c,d\\}. $$$
Lean4
theorem convexJoin_segments (a b c d : E) :
convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = convexHull 𝕜 { a, b, c, d } := by
simp_rw [← convexHull_pair, convexHull_insert (insert_nonempty _ _), convexHull_insert (singleton_nonempty _),
convexJoin_assoc, convexHull_singleton]
