lt_ofReal_iff_toReal_lt — Mathlib

English

For a finite ENNReal a (a ≠ ∞), and any real b, a < ENNReal.ofReal(b) if and only if toReal(a) < b.

Русский

Для конечного ENNReal a (a ≠ ∞) и любого действительного b верно: a < ENNReal.ofReal(b) ⇔ toReal(a) < b.

LaTeX

$$$a \neq \infty \Rightarrow a < \operatorname{ofReal}(b) \iff \operatorname{toReal}(a) < b$$$

Lean4

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

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