English
Let z,w ∈ ℂ. The rectangle with corners z and w is the axis-parallel rectangle consisting of all points x ∈ ℂ whose real part lies between Re z and Re w and whose imaginary part lies between Im z and Im w.
Русский
Пусть z, w ∈ ℂ. Прямоугольник с вершинами z и w — это осесимметричный прямоугольник на комплексной плоскости, состоящий из всех точек x ∈ ℂ такие что Re x ∈ [Re z, Re w] и Im x ∈ [Im z, Im w].
LaTeX
$$$$ \{ x \in \mathbb{C} : \Re x \in [\Re z, \Re w] \wedge \Im x \in [\Im z, \Im w] \} $$$$
Lean4
/-- A `Rectangle` is an axis-parallel rectangle with corners `z` and `w`. -/
def Rectangle (z w : ℂ) : Set ℂ :=
[[z.re, w.re]] ×ℂ [[z.im, w.im]]
