ofReal_mem_slitPlane — Mathlib

English

For every real x, the complex number formed by embedding x into the complex plane lies in slitPlane if and only if x > 0.

Русский

Пусть x ∈ ℝ. Комплексное число, получаемое вкладыванием x в ℂ, принадлежит слитной плоскости тогда и только тогда, когда x > 0.

LaTeX

$$$\\uparrow x \\in \\text{slitPlane} \\iff 0 < x$$$

Lean4

@[simp]
theorem ofReal_mem_slitPlane {x : ℝ} : ↑x ∈ slitPlane ↔ 0 < x := by simp [mem_slitPlane_iff]

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