lt_iff_exists_real_btwn — Mathlib

English

For ENNReal a < b, there exists a real r with 0 ≤ r and a < ENNReal.ofReal r and ENNReal.ofReal r < b.

Русский

Для a < b существует действительное число r с 0 ≤ r и a < ENNReal.ofReal r и ENNReal.ofReal r < b.

LaTeX

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

Lean4

theorem lt_iff_exists_real_btwn : a < b ↔ ∃ r : ℝ, 0 ≤ r ∧ a < ENNReal.ofReal r ∧ (ENNReal.ofReal r : ℝ≥0∞) < b :=
  ⟨fun h =>
    let ⟨q, q0, aq, qb⟩ := ENNReal.lt_iff_exists_rat_btwn.1 h
    ⟨q, Rat.cast_nonneg.2 q0, aq, qb⟩,
    fun ⟨_, _, qa, qb⟩ => lt_trans qa qb⟩

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