ofReal_lt_iff_lt_toReal — Mathlib

English

For a ≥ 0 and b not infinite, ENNReal.ofReal a < b iff a < b.toReal.

Русский

Для a ≥ 0 и b ≠ ∞: ENNReal.ofReal a < b ↔ a < b.toReal.

LaTeX

$$$ a \ge 0 \land b ≠ \infty \Rightarrow ENNReal.ofReal a < b \iff a < b.toReal $$$

Lean4

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

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