nonneg_iff — Mathlib

English

An element z lies in the nonnegative cone of the complex-like space if and only if z is real and its imaginary part is zero and its real part is nonnegative.

Русский

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

LaTeX

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

Lean4

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

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