natCast_natAbs — Mathlib

English

For any integer n, the nonnegative real cast of its natAbs equals the NNReal norm, i.e., (n.natAbs : ℝ≥0) = ∥n∥₊.

Русский

Для любого n ∈ ℤ невершод natAbs отображается в ℝ≥0 так же, как и норма ∥n∥₊: (n.natAbs : ℝ≥0) = ∥n∥₊.

LaTeX

$$$(n.natAbs : \mathbb{R}_{\ge 0}) = \|n\|_{+}$$$

Lean4

theorem _root_.NNReal.natCast_natAbs (n : ℤ) : (n.natAbs : ℝ≥0) = ‖n‖₊ :=
  NNReal.eq <|
    calc
      ((n.natAbs : ℝ≥0) : ℝ) = (n.natAbs : ℤ) := by simp only [Int.cast_natCast, NNReal.coe_natCast]
      _ = |(n : ℝ)| := by simp only [Int.natCast_natAbs, Int.cast_abs]
      _ = ‖n‖ := (norm_eq_abs n).symm

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