English
Let x be a boundary parameter from the extended real line. The set of complex numbers with imaginary part strictly less than x is an open subset of the complex plane.
Русский
Пусть x является границей на плоскости из расширенного действительного числа. Множество комплексных чисел z с условием Im(z) < x является открытым подмножеством комплексной плоскости.
LaTeX
$$$\\forall x \\in \\overline{\\mathbb{R}},\\; \\{z \\in \\mathbb{C} : \\operatorname{Im}(z) < x\\} \\text{ открыто в } \\mathbb{C}. $$$
Lean4
/-- An open lower half-plane (with boundary imaginary part given by an `EReal`) is an open set
in the complex plane. -/
theorem isOpen_im_lt_EReal (x : EReal) : IsOpen {z : ℂ | z.im < x} :=
isOpen_lt (EReal.continuous_coe_iff.mpr continuous_im) continuous_const
