English
For every natural number n, the NNReal value obtained by viewing n as ENNReal and applying toNNReal is n.
Русский
Для любого натурального числа n значение NNReal, получаемое путём представления n как ENNReal и применения toNNReal, равно n.
LaTeX
$$$ (n : \\mathbb{R}_{\\ge 0}^\\infty).toNNReal = (n : \\mathbb{R}_{\\ge 0}) $$$
Lean4
@[simp, norm_cast]
theorem toNNReal_natCast (n : ℕ) : (n : ℝ≥0∞).toNNReal = n := by rw [← ENNReal.coe_natCast n, ENNReal.toNNReal_coe]