English
For ENNReal a < b, there exists a rational q with 0 ≤ q and a < Real.toNNReal q and Real.toNNReal q < b.
Русский
Для ENNReal a < b существует рациональное q, такое что 0 ≤ q и a < Real.toNNReal q и Real.toNNReal q < b.
LaTeX
$$$ a < b \iff \exists q : \\mathbb{Q}, 0 \le q \land a < Real.toNNReal q \land (Real.toNNReal q : \\mathbb{R}_{\\ge 0}^\\infty) < b $$$
Lean4
theorem lt_iff_exists_rat_btwn : a < b ↔ ∃ q : ℚ, 0 ≤ q ∧ a < Real.toNNReal q ∧ (Real.toNNReal q : ℝ≥0∞) < b :=
⟨fun h => by
rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩
rcases exists_between h with ⟨c, pc, cb⟩
rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩
rcases (NNReal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩
exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩, fun ⟨_, _, qa, qb⟩ => lt_trans qa qb⟩
