toNNReal_natCast_eq_toNNReal

Mathlib.Data.ENNReal.Basic

URI: https://scilib.ai/kg/mathlib#ENNReal.toNNReal_natCast_eq_toNNReal

← MathLib Explorer

English

For any natural n, (n : ENNReal).toNNReal equals (n : Real).toNNReal.

Русский

Для любого натурального n, (n : ENNReal).toNNReal равно (n : Real).toNNReal.

LaTeX

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

Lean4

theorem toNNReal_natCast_eq_toNNReal (n : ℕ) : (n : ℝ≥0∞).toNNReal = (n : ℝ).toNNReal := by
  rw [Real.toNNReal_of_nonneg (by positivity), ENNReal.toNNReal_natCast, mk_natCast]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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