mem_slitPlane_iff — Mathlib

English

For any z ∈ ℂ, z lies in the slit plane if and only if 0 < Re z or Im z ≠ 0.

Русский

Для любого z ∈ ℂ верно: z принадлежит щельной плоскости тогда и только тогда, когда 0 < Re z или Im z ≠ 0.

LaTeX

$$$ z \\in \\text{slitPlane} \\iff 0 < \\operatorname{Re}(z) \\; \\lor\\; \\operatorname{Im}(z) \\neq 0 $$$

Lean4

theorem mem_slitPlane_iff {z : ℂ} : z ∈ slitPlane ↔ 0 < z.re ∨ z.im ≠ 0 :=
  Set.mem_setOf

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