ofNNReal_toNNReal

Mathlib.Data.ENNReal.Basic

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

English

For x ∈ Real, (Real.toNNReal x : ENNReal) = ENNReal.ofReal x.

Русский

Для x ∈ Real, (Real.toNNReal x : ENNReal) = ENNReal.ofReal x.

LaTeX

$$$ (Real.toNNReal x : ENNReal) = ENNReal.ofReal x $$$

Lean4

theorem ofNNReal_toNNReal (x : ℝ) : (Real.toNNReal x : ℝ≥0∞) = ENNReal.ofReal x :=
  rfl

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

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

Разделы

Аффилиация

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