toENNReal_ofNat — Mathlib

English

For n ≥ 2, the natural-number literal of n in ENnReal equals its ENNReal interpretation; the embedding respects literals for n with AtLeastTwo.

Русский

Для n ≥ 2, буквальное представление натурального числа n в ENNReal равно его векторному отображению в ENNReal; встраивание сохраняет литералы для n≥2.

LaTeX

$$$((\\mathrm{ofNat}(n) : \\mathbb{N}_\\infty) : \\mathbb{R}_{\\ge 0,\\infty}) = \\mathrm{ofNat}(n) \\\\ \\text{для } n \\ge 2.$$$

Lean4

@[simp, norm_cast]
theorem toENNReal_ofNat (n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℕ∞) : ℝ≥0∞) = ofNat(n) :=
  rfl

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