Density of Q in R

Stream: Is there code for X?

[Bhavik Mehta]

I'm struggling to find the statement that between any two different reals there's a rational but I find it hard to believe no-one's done it yet! Any help?

[Mario Carneiro]

It's in algebra.archimedean

[Mario Carneiro]

exists_rat_btwn

[Patrick Massot]

import analysis.normed_space.basic -- Just to make sure we have everything about real numbers

example (x y : ℝ) (h : x < y): ∃ z : ℚ, x < z ∧ (z : ℝ) < y :=
by library_search

[Patrick Massot]

But it doesn't feel right that this is not in data.real.basic

[Mario Carneiro]

It used to be, but it is generalized to archimedean fields now

[Mario Carneiro]

This is standard practice elsewhere in algebra

[Bhavik Mehta]

Thanks!