Stream: Is there code for X?
Topic: Density of Q in R
Bhavik Mehta (Apr 17 2020 at 11:03):
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 (Apr 17 2020 at 11:15):
Mario Carneiro (Apr 17 2020 at 11:16):
Patrick Massot (Apr 17 2020 at 11:18):
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 (Apr 17 2020 at 11:19):
But it doesn't feel right that this is not in
Mario Carneiro (Apr 17 2020 at 11:19):
It used to be, but it is generalized to archimedean fields now
Mario Carneiro (Apr 17 2020 at 11:20):
This is standard practice elsewhere in
Bhavik Mehta (Apr 17 2020 at 13:11):
Last updated: May 16 2021 at 05:21 UTC