isOpen_re_gt_EReal — Mathlib

English

An open right half-plane {z ∈ ℂ | x < z.re} is open in ℂ.

Русский

Правая открытая полуплоскость {z ∈ ℂ | x < z.re} открыта в ℂ.

LaTeX

$$$\\\\IsOpen\\\\{z ∈ \\mathbb{C} : x < \\Re z\\\\}$$$

Lean4

/-- An open right half-plane (with boundary real part given by an `EReal`) is an open set
in the complex plane. -/
theorem isOpen_re_gt_EReal (x : EReal) : IsOpen {z : ℂ | x < z.re} :=
  isOpen_lt continuous_const <| EReal.continuous_coe_iff.mpr continuous_re

Похожие утверждения