slitPlane_eq_union — Mathlib

English

The slit plane is the union of the right half-plane and the set where the imaginary part is nonzero.

Русский

Щельная плоскость равна объединению правой полуплоскости и множества, где мнимая часть не равна нулю.

LaTeX

$$$ \\text{slitPlane} = \\{ z \\in \\mathbb{C} : \\operatorname{Re}(z) > 0 \\} \\cup \\{ z \\in \\mathbb{C} : \\operatorname{Im}(z) \\neq 0 \\} $$$

Lean4

theorem slitPlane_eq_union : slitPlane = {z | 0 < z.re} ∪ {z | z.im ≠ 0} :=
  Set.setOf_or.symm

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