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⟩