lt_iff_exists_nnreal_btwn — Mathlib

English

For ENNReal a < b, there exists r ∈ ℝ_{≥0} with a < r and (r : ENNReal) < b.

Русский

Для a < b существует r ∈ ℝ_{≥0}, такое что a < r и (r : ENNReal) < b.

LaTeX

$$$ a < b \iff \exists r : \mathbb{R}_{\\ge 0}, a < (r : \\mathbb{R}_{\\ge 0}^\\infty) \land (r : \\mathbb{R}_{\\ge 0}^\\infty) < b $$$

Lean4

theorem lt_iff_exists_nnreal_btwn : a < b ↔ ∃ r : ℝ≥0, a < r ∧ (r : ℝ≥0∞) < b :=
  WithTop.lt_iff_exists_coe_btwn

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