nonneg_iff_normalize_eq_self — Mathlib

English

Normalization equals the identity exactly for nonnegative numbers: normalize(z) = z iff z ≥ 0.

Русский

Нормализация равна тождественному отображению только для неотрицательных чисел: normalize(z) = z тогда и только тогда, когда z ≥ 0.

LaTeX

$$$\operatorname{normalize}(z) = z \iff 0 \le z$$$

Lean4

theorem nonneg_iff_normalize_eq_self (z : ℤ) : normalize z = z ↔ 0 ≤ z :=
  ⟨nonneg_of_normalize_eq_self, normalize_of_nonneg⟩

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