(* begin hide *)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/CReals_is_CReals.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/CReals_is_CReals.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/Lim_Cauchy.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/Lim_Cauchy.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/Archimedes.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/Archimedes.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/Archimedes'.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/Archimedes'.con" as lemma.
(*#**************************************)
To define the injection we need one elemntary lemma about the denominator:
*)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/den_is_nonzero.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/den_is_nonzero.con" as lemma.
(*#* 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]. *)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q.con" as definition.
(*#* Next we need some properties of [nring], on the setoid of natural numbers: *)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_strext.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_strext.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_wd.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_wd.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_eq.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_eq.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_leEq.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_leEq.con" as lemma.
(* begin hide *)
(*#* Similarly we prove some properties of [zring] on the ring of integers: *)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/zring_strext.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/zring_strext.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/zring_wd.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/zring_wd.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/zring_less.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/zring_less.con" as lemma.
(*#* 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. *)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_strext.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_strext.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_wd.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_wd.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_plus.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_plus.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_mult.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_mult.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_less.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_less.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/less_inj_Q.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/less_inj_Q.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/leEq_inj_Q.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/leEq_inj_Q.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_leEq.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_leEq.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_min.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_min.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_minus.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_minus.con" as lemma.
(*#* Moreover, and as expected, the [AbsSmall] predicate is also
preserved under the [inj_Q] *)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_AbsSmall.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_AbsSmall.con" as lemma.
-inline procedural "cic:/CoRN/reals/Q_in_CReals/AbsSmall_inj_Q.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/AbsSmall_inj_Q.con" as lemma.
(*#* ** 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].
*)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_Cauchy.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_Cauchy.con" as theorem.
(*#* 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]:
*)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_nring.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_nring.con" as lemma.
(*#* ** Injection of [Q] is dense
Finally we are able to prove the density of image of [Q] in [R1]. We
trisection" argument, which is ubiquitous in constructive analysis.
*)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/start_of_sequence.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/start_of_sequence.con" as theorem.
(*#* 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. *)
-inline procedural "cic:/CoRN/reals/Q_in_CReals/Q_dense_in_CReals.con".
+inline procedural "cic:/CoRN/reals/Q_in_CReals/Q_dense_in_CReals.con" as lemma.
(* UNEXPORTED
End Rational_sequence_prelogue