toReal_natCast — Mathlib

English

For every natural n, the real value of n viewed as ENNReal equals n.

Русский

Для каждого натурального n вещественное значение числа, полученное представлением n как ENNReal и взятием toReal, равно n.

LaTeX

$$$ (n : \\mathbb{R}_{\\ge 0}^\\infty).toReal = n $$$

Lean4

@[simp, norm_cast]
theorem toReal_natCast (n : ℕ) : (n : ℝ≥0∞).toReal = n := by
  rw [← ENNReal.ofReal_natCast n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)]

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