ofReal_eq_coe_nnreal

Mathlib.Data.ENNReal.Basic

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

English

For x ∈ Real with h ≥ 0, ENNReal.ofReal x = ENNReal.ofNNReal ⟨x,h⟩.

Русский

Для x ∈ Real с ∧ h ≥ 0, ENNReal.ofReal x = ENNReal.ofNNReal ⟨x,h⟩.

LaTeX

$$$\text{If } x \ge 0,\quad ENNReal.ofReal(x) = ENNReal.ofNNReal\langle x, h \rangle$$$

Lean4

theorem ofReal_eq_coe_nnreal {x : ℝ} (h : 0 ≤ x) : ENNReal.ofReal x = ofNNReal ⟨x, h⟩ :=
  (coe_nnreal_eq ⟨x, h⟩).symm

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

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

Разделы

Аффилиация

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