coe_nnreal_eq

Mathlib.Data.ENNReal.Basic

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

English

For r ∈ ℝ≥0, (r : ENNReal) = ENNReal.ofReal r.toReal.

Русский

Для r ∈ ℝ≥0, (r : ENNReal) = ENNReal.ofReal r.toReal.

LaTeX

$$$ (r : ENNReal) = ENNReal.ofReal(r.toReal) $$$

Lean4

theorem coe_nnreal_eq (r : ℝ≥0) : (r : ℝ≥0∞) = ENNReal.ofReal r := by rw [ENNReal.ofReal, Real.toNNReal_coe]

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

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

Разделы

Аффилиация

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