toNNReal_natCast — Mathlib

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]

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