English
A rectangle with opposite corners z and w is equal to the convex hull of its four corner points: z, z.re + w.im i, w.re + z.im i, and w.
Русский
Прямоугольник с противоположными вершинами z и w равен выпуклой оболочке его четырех вершин: z, z.re + w.im i, w.re + z.im i, и w.
LaTeX
$$$\\text{Rectangle}(z,w) = \\operatorname{conv}_{\\mathbb{R}}\\{ z, \\Re(z) + \\Im(w)i, \\Re(w) + \\Im(z)i, w \\}$$$
Lean4
theorem rectangle_eq_convexHull (z w : ℂ) : Rectangle z w = convexHull ℝ {z, z.re + w.im * I, w.re + z.im * I, w} := by
simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm, ← preimage_equivRealProd_prod,
insert_prod, singleton_prod, image_pair, insert_union, ← insert_eq, preimage_equiv_eq_image_symm, image_insert_eq,
image_singleton, equivRealProd_symm_apply, re_add_im]
