On density of the image of Q in an arbitrary real number structure

In this file we introduce the image of the concrete rational numbers (as defined earlier) in an arbitrary structure of type CReals. At the end of this file we assign to any real number two rational numbers for which the real number lies betwen image of them; in other words we will prove that the image of rational numbers in dense in any real number structure.

Let R1 be a real number structure.

Injection from Q to an arbitrary real number structure

First we need to define the injection from Q to R1. Note that in Cauchy_CReals we defined inject_Q from an arbitray field F to (R_COrdField F) which was the set of Cauchy sequences of that field. But since R1 is an arbitrary real number structure we can not use inject_Q.

To define the injection we need one elemntary lemma about the denominator:

And we define the injection in the natural way, using zring and nring. We call this inj_Q, in contrast with inject_Q defined in Cauchy_CReals.

Next we need some properties of nring, on the setoid of natural numbers:

Similarly we prove some properties of zring on the ring of integers:

Using the above lemmata we prove the basic properties of inj_Q, i.e. it is a setoid function and preserves the ring operations and oreder operation.

Moreover, and as expected, the AbsSmall predicate is also preserved under the inj_Q

Injection preserves Cauchy property

We apply the above lemmata to obtain following theorem, which says that a Cauchy sequence of elemnts of Q will be Cauchy in R1.

Furthermore we prove that applying nring (which is adding the ring unit n times) is the same whether we do it in Q or in R1:

Injection of Q is dense

Finally we are able to prove the density of image of Q in R1. We state this fact in two different ways. Both of them have their specific use.

The first theorem states the fact that any real number can be bound by the image of two rational numbers. This is called start_of_sequence because it can be used as an starting point for the typical "interval trisection" argument, which is ubiquitous in constructive analysis.

The second version of the density of Q in R1 states that given any positive real number, there is a rational number between it and zero. This lemma can be used to prove the more general fact that there is a rational number between any two real numbers.