The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Thank you all for your suggestions.

What I meant by "dense" was that between any two real numbers there is another real number. It turned out that it was easier to prove than I initially thought:

Lemma density_of_reals (x y : R): (x < y -> exists z : R, x < z < y)%R.
Proof.
  intro H.
  exists ((x+y)/2)%R.
  lra.
Qed.

On Tue, Oct 1, 2013 at 11:54 AM, Daniel Schepler <dschepler AT gmail.com> wrote:

On Tue, Oct 1, 2013 at 5:42 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

2013/10/1 Jason Gross <jasongross9 AT gmail.com>

I assume that by "dense", the desired theorem is that between every two non-equal rational numbers there's a real number.  This is very easy, though: just convert their average to a real number.  Alternatively, you might want the theorem that the irrationals are dense in the rationals (between every two non-equal rationals there is an irrational); I don't know how to prove this).

Hmm, wouldn't it be better to say that "the irrationals are dense in the reals"? As far as I remember, "X is dense IN Y" implies that X is a subset of Y (else, they are not "<some property> IN").
And for that last proof, it should not be hard. Take two rationals x and y such that x<y, x+π⁻¹×(y-x) is irrational (else by stability of the usual operations, that would mean that ((x+π⁻¹×(y-x))×(y-x)⁻¹-x)⁻¹ = π would be rational.
Furthermore, as 0<π⁻¹<1, 0<π⁻¹×(y-x)<y-x, and so x<x+π⁻¹×(y-x)<y.

And if what you want is a proof that the rationals are dense in the reals, see
<URL:http://coq.inria.fr/pylons/contribs/files/Topology/v8.4/Topology.RationalsInReals.html#rationals_dense_in_reals>
--

Daniel Schepler