coe_toENNReal — Mathlib

English

If x ≥ 0, then (x.toENNReal) viewed as an EReal equals x.

Русский

Если x ≥ 0, то (x.toENNReal), трактуемое как элемент EReal, равно x.

LaTeX

$$$ (x.toENNReal : \mathrm{EReal}) = x \quad \text{for } x \ge 0 $$$

Lean4

@[simp]
theorem coe_toENNReal {x : EReal} (hx : 0 ≤ x) : (x.toENNReal : EReal) = x :=
  by
  rw [toENNReal]
  by_cases h_top : x = ⊤
  · rw [if_pos h_top, h_top]
    rfl
  rw [if_neg h_top]
  simp only [coe_ennreal_ofReal, hx, toReal_nonneg, max_eq_left]
  exact coe_toReal h_top fun _ ↦ by simp_all only [le_bot_iff, zero_ne_bot]

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