toNat_add_toNat_neg_eq_nnnorm — Mathlib

English

For any integer n, the sum of the nonnegative parts of n and −n equals the NN-norm of n.

Русский

Для любого целого числа n сумма неотрицательных частей n и −n равна nnnorm(n).

LaTeX

$$$ \\max(n,0) + \\max(-n,0) = |n| \\,=\, \\|n\\|_{+} $$$

Lean4

@[simp]
theorem toNat_add_toNat_neg_eq_nnnorm (n : ℤ) : ↑n.toNat + ↑(-n).toNat = ‖n‖₊ := by
  rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.natCast_natAbs]

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