nonneg_iff — Mathlib

English

For z ∈ ℂ, z is nonnegative in the complex order if and only if its real part is nonnegative and its imaginary part is zero: Re(z) ≥ 0 and Im(z) = 0.

Русский

Для z ∈ ℂ неотрицательность по порядку комплексных чисел эквивалентна тому, что Re(z) ≥ 0 и Im(z) = 0.

LaTeX

$$$$ 0 \le z \iff 0 \le \Re(z) \land 0 = \Im(z) $$$$

Lean4

theorem nonneg_iff {z : ℂ} : 0 ≤ z ↔ 0 ≤ z.re ∧ 0 = z.im :=
  le_def

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