English
For a,b ∈ ℝ≥0 there exists a rational q with 0 ≤ q such that a < Real.toNNReal q < b iff a < b.
Русский
Для a,b ∈ ℝ≥0 существует рациональный q с 0 ≤ q и a < Real.toNNReal q < b тогда и только тогда, когда a < b.
LaTeX
$$$ a < b \\; \\iff \\; \\exists q \\in \\mathbb{Q}, 0 \\le q \\land a < \\operatorname{Real.toNNReal}(q) \\land \\operatorname{Real.toNNReal}(q) < b. $$$
Lean4
theorem lt_iff_exists_rat_btwn (a b : ℝ≥0) : a < b ↔ ∃ q : ℚ, 0 ≤ q ∧ a < Real.toNNReal q ∧ Real.toNNReal q < b :=
Iff.intro
(fun h : (↑a : ℝ) < (↑b : ℝ) =>
let ⟨q, haq, hqb⟩ := exists_rat_btwn h
have : 0 ≤ (q : ℝ) := le_trans a.2 <| le_of_lt haq
⟨q, Rat.cast_nonneg.1 this, by simp [Real.coe_toNNReal _ this, NNReal.coe_lt_coe.symm, haq, hqb]⟩)
fun ⟨_, _, haq, hqb⟩ => lt_trans haq hqb
