pos_iff — Mathlib

English

An element z is positive in the complex-like order if and only if z is a positive real number and has zero imaginary part.

Русский

Элемент z положителен в комплексоподобном порядке тогда и только тогда, когда z — положительное вещественное число и Im(z) = 0.

LaTeX

$$$ 0 < z \iff \bigl( 0 < \operatorname{re}(z) \bigr) \land \operatorname{im}(z) = 0 $$$

Lean4

theorem pos_iff : 0 < z ↔ 0 < re z ∧ im z = 0 := by simpa only [map_zero, eq_comm] using lt_iff_re_im (z := 0) (w := z)

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