ofReal_coe_nnreal

Mathlib.Data.ENNReal.Basic

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

English

For p ∈ NNReal, ENNReal.ofReal p = p.

Русский

Для p ∈ NNReal, ENNReal.ofReal p = p.

LaTeX

$$$ ENNReal.ofReal p = p $$$

Lean4

@[simp]
theorem ofReal_coe_nnreal : ENNReal.ofReal p = p :=
  (coe_nnreal_eq p).symm

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

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

Разделы

Аффилиация

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