Zulip Chat Archive

Stream: Is there code for X?

Topic: Density of Q in R


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 17 2020 at 11:15):

It's in algebra.archimedean

view this post on Zulip Mario Carneiro (Apr 17 2020 at 11:16):

exists_rat_btwn

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 17 2020 at 11:19):

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

view this post on Zulip Mario Carneiro (Apr 17 2020 at 11:19):

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

view this post on Zulip Mario Carneiro (Apr 17 2020 at 11:20):

This is standard practice elsewhere in algebra

view this post on Zulip Bhavik Mehta (Apr 17 2020 at 13:11):

Thanks!


Last updated: May 16 2021 at 05:21 UTC