pos_iff

Mathlib.Analysis.Complex.Order

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

English

In the chosen complex order, z > 0 iff its real part is positive and its imaginary part is zero.

Русский

В выбранном порядке комплексного поля z > 0 тогда и только тогда, когда вещественная часть положительна и мнимая равна нулю.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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