neg_ofReal_mem_slitPlane

Mathlib.Analysis.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.neg_ofReal_mem_slitPlane

English

For every real x, the complex number −x lies in slitPlane if and only if x < 0.

Русский

Для любого x ∈ ℝ число −x (как комплекс) принадлежит слитной плоскости тогда и только тогда, когда x < 0.

LaTeX

$$-↑x ∈ \\text{slitPlane} \\iff x < 0$$

Lean4

@[simp]
theorem neg_ofReal_mem_slitPlane {x : ℝ} : -↑x ∈ slitPlane ↔ x < 0 := by simpa using ofReal_mem_slitPlane (x := -x)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru