nonpos_iff — Mathlib

English

An element z satisfies z ≤ 0 if and only if z is a nonpositive real number with zero imaginary part.

Русский

Элемент z удовлетворяет z ≤ 0 тогда и только тогда, когда z — неположительное вещественное число с нулевой мнимой частью.

LaTeX

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

Lean4

theorem nonpos_iff : z ≤ 0 ↔ re z ≤ 0 ∧ im z = 0 := by simpa only [map_zero] using le_iff_re_im (z := z) (w := 0)

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