toENNReal_coe

Mathlib.Data.Real.ENatENNReal

URI: https://scilib.ai/kg/mathlib#ENat.toENNReal_coe

English

For every natural number n, the natural embedding of n into ENNReal agrees with the corresponding numeral n in ENNReal.

Русский

Для каждого естественного числа n встраивание n в ENNReal совпадает с тем же числом в ENNReal.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem toENNReal_coe (n : ℕ) : ((n : ℕ∞) : ℝ≥0∞) = n :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru