toENNReal_coe — Mathlib

English

For any x ∈ ENNReal, (x : EReal).toENNReal = x.

Русский

Для любого x ∈ ENNReal, если рассмотреть x как элемент EReal, то toENNReal возвращает x.

LaTeX

$$$ \operatorname{toENNReal}((x : \mathrm{EReal})) = x $$$

Lean4

@[simp]
theorem toENNReal_coe {x : ℝ≥0∞} : (x : EReal).toENNReal = x :=
  by
  by_cases h_top : x = ⊤
  · rw [h_top, coe_ennreal_top, toENNReal_top]
  rwa [toENNReal, if_neg _, toReal_coe_ennreal, ENNReal.ofReal_toReal_eq_iff]
  simp [h_top]

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