English
Between any a < b in EReal there exists q ∈ ℚ with a < q < b.
Русский
Между любыми a < b в EReal существует q ∈ ℚ такие, что a < q < b.
LaTeX
$$$ \forall a,b : \mathrm{EReal},\ a < b \Rightarrow \exists q \in \mathbb{Q},\ a < (q : \mathbb{R}) \land ((q : \mathbb{R}) : \mathrm{EReal}) < b $$$
Lean4
theorem exists_rat_btwn_of_lt : ∀ {a b : EReal}, a < b → ∃ x : ℚ, a < (x : ℝ) ∧ ((x : ℝ) : EReal) < b
| ⊤, _, h => (not_top_lt h).elim
| (a : ℝ), ⊥, h => (lt_irrefl _ ((bot_lt_coe a).trans h)).elim
| (a : ℝ), (b : ℝ), h => by simp [exists_rat_btwn (EReal.coe_lt_coe_iff.1 h)]
| (a : ℝ), ⊤, _ =>
let ⟨b, hab⟩ := exists_rat_gt a
⟨b, by simpa using hab, coe_lt_top _⟩
| ⊥, ⊥, h => (lt_irrefl _ h).elim
| ⊥, (a : ℝ), _ =>
let ⟨b, hab⟩ := exists_rat_lt a
⟨b, bot_lt_coe _, by simpa using hab⟩
| ⊥, ⊤, _ => ⟨0, bot_lt_coe _, coe_lt_top _⟩
