toNat_add_toNat_neg_eq_norm — Mathlib

English

For every integer n, the real absolute value equals the sum of the nonnegative parts, interpreted in real.

Русский

Для каждого целого числа n модуль имеет представление как сумма неотрицательных частей, рассмотренное в вещественном поле.

LaTeX

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

Lean4

@[simp]
theorem toNat_add_toNat_neg_eq_norm (n : ℤ) : ↑n.toNat + ↑(-n).toNat = ‖n‖ := by
  simpa only [NNReal.coe_natCast, NNReal.coe_add] using congrArg NNReal.toReal (toNat_add_toNat_neg_eq_nnnorm n)

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