neg_iff — Mathlib

English

An element z is strictly negative if and only if z is a negative real and has zero imaginary part.

Русский

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

LaTeX

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

Lean4

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

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