English
For any a < b in EReal, a < b iff there exists q ∈ ℚ with a < (q : ℝ) and (q : ℝ) < b.
Русский
Для любых a < b в EReal, a < b эквивалентно существованию q ∈ ℚ с a < (q : ℝ) и (q : ℝ) < b.
LaTeX
$$$ a < b \iff \exists q \in \mathbb{Q}, a < (q : \mathbb{R}) \land ((q : \mathbb{R}) : \mathrm{EReal}) < b $$$
Lean4
theorem lt_iff_exists_rat_btwn {a b : EReal} : a < b ↔ ∃ x : ℚ, a < (x : ℝ) ∧ ((x : ℝ) : EReal) < b :=
⟨fun hab => exists_rat_btwn_of_lt hab, fun ⟨_x, ax, xb⟩ => ax.trans xb⟩