mem_slitPlane_iff_not_le_zero

Mathlib.Analysis.Complex.Basic

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

English

For any z ∈ ℂ, z ∈ slitPlane iff z is not ≤ 0.

Русский

Для любого z ∈ ℂ верно, что z ∈ slitPlane тогда и только тогда, когда z не ≤ 0.

LaTeX

$$z \\in \\text{slitPlane} \\iff \\lnot (z \\le 0)$$

Lean4

theorem mem_slitPlane_iff_not_le_zero {z : ℂ} : z ∈ slitPlane ↔ ¬z ≤ 0 :=
  mem_slitPlane_iff.trans not_le_zero_iff.symm

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

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

Разделы

Аффилиация

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