neg_iff

Mathlib.Analysis.Complex.Order

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

English

z < 0 iff z.re < 0 and z.im = 0.

Русский

z < 0 тогда и только тогда, когда z.re < 0 и z.im = 0.

LaTeX

$$$z < 0 \iff z_{re} < 0 \land z_{im} = 0$$$

Lean4

theorem neg_iff {z : ℂ} : z < 0 ↔ z.re < 0 ∧ z.im = 0 :=
  lt_def

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

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

Разделы

Аффилиация

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