le_ofReal_iff_toReal_le — Mathlib

English

For a finite ENNReal element a (a ≠ ∞) and any real b ≥ 0, the inequality a ≤ ofReal(b) in ENNReal is equivalent to the real inequality toReal(a) ≤ b.

Русский

Для конечного элемента ENNReal a (a ≠ ∞) и любого действительного b ≥ 0 неравенство a ≤ ofReal(b) в ENNReal эквивалентно неравенству toReal(a) ≤ b в ℝ.

LaTeX

$$$a \neq \infty \quad\&\&\quad 0 \le b \Rightarrow a \le \operatorname{ofReal}(b) \iff \operatorname{toReal}(a) \le b$$

Lean4

theorem le_ofReal_iff_toReal_le {a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ∞) (hb : 0 ≤ b) :
    a ≤ ENNReal.ofReal b ↔ ENNReal.toReal a ≤ b :=
  by
  lift a to ℝ≥0 using ha
  simpa [ENNReal.ofReal, ENNReal.toReal] using Real.le_toNNReal_iff_coe_le hb

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