English
If U is convex and z,w ∈ U and the two other corners z.re + w.im i and w.re + z.im i also lie in U, then the entire rectangle with corners z and w lies in U.
Русский
Если U выпукло и z,w ∈ U, а также остальные два угла z.re + w.im i и w.re + z.im i лежат в U, то весь прямоугольник, образованный z и w, содержится в U.
LaTeX
$$Если U выпукло и z,w ∈ U, а (z.re + w.im i) ∈ U и (w.re + z.im i) ∈ U, то Rectangle(z,w) ⊆ U.$$
Lean4
/-- If opposite corners of a rectangle are contained in a convex set, the whole rectangle is. -/
theorem rectangle_subset {U : Set ℂ} (U_convex : Convex ℝ U) {z w : ℂ} (hz : z ∈ U) (hw : w ∈ U)
(hzw : (z.re + w.im * I) ∈ U) (hwz : (w.re + z.im * I) ∈ U) : Rectangle z w ⊆ U := by
simpa only [rectangle_eq_convexHull] using convexHull_min (by grind) U_convex
