mem_slitPlane_iff_arg — Mathlib

English

An element z belongs to the slit plane if and only if z ≠ 0 and arg z ≠ π; equivalently, z ∈ slitPlane ⇔ z.arg ≠ π ∧ z ≠ 0.

Русский

Элемент z принадлежит слитой плоскости тогда и только тогда, когда z ≠ 0 и z.arg ≠ π; тождественно, z ∈ slitPlane ⇔ z.arg ≠ π ∧ z ≠ 0.

LaTeX

$$$ z \in \text{slitPlane} \;\Longleftrightarrow\; z.arg \neq \pi \wedge z \neq 0 $$$

Lean4

/-- An alternative description of the slit plane as consisting of nonzero complex numbers
whose argument is not π. -/
theorem mem_slitPlane_iff_arg {z : ℂ} : z ∈ slitPlane ↔ z.arg ≠ π ∧ z ≠ 0 := by
  simp only [mem_slitPlane_iff_not_le_zero, le_iff_lt_or_eq, ne_eq, arg_eq_pi_iff_lt_zero, not_or]

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