X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Freals%2FQ_in_CReals.ma;h=a9beac518fe7084525af1864cf29437735fbbace;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=8a803f4357f5ef840819d9775f32498ee8d2096d;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma b/helm/software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma index 8a803f435..a9beac518 100644 --- a/helm/software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma +++ b/helm/software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma @@ -16,6 +16,8 @@ set "baseuri" "cic:/matita/CoRN-Decl/reals/Q_in_CReals". +include "CoRN.ma". + (* $Id: Q_in_CReals.v,v 1.10 2004/04/23 10:01:05 lcf Exp $ *) (*#* * On density of the image of [Q] in an arbitrary real number structure @@ -26,17 +28,11 @@ 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. *) -(* INCLUDE -Cauchy_IR -*) +include "model/reals/Cauchy_IR.ma". -(* INCLUDE -Nmonoid -*) +include "model/monoids/Nmonoid.ma". -(* INCLUDE -Zring -*) +include "model/rings/Zring.ma". (* UNEXPORTED Section Rational_sequence_prelogue. @@ -47,22 +43,24 @@ Section Rational_sequence_prelogue. %\end{convention}% *) -inline cic:/CoRN/reals/Q_in_CReals/R1.var. +inline "cic:/CoRN/reals/Q_in_CReals/R1.var". (* We clone these proofs from CReals1.v just because there IR is an axiom *) (* begin hide *) -inline cic:/CoRN/reals/Q_in_CReals/CReals_is_CReals.con. +inline "cic:/CoRN/reals/Q_in_CReals/CReals_is_CReals.con". -inline cic:/CoRN/reals/Q_in_CReals/Lim_Cauchy.con. +inline "cic:/CoRN/reals/Q_in_CReals/Lim_Cauchy.con". -inline cic:/CoRN/reals/Q_in_CReals/Archimedes.con. +inline "cic:/CoRN/reals/Q_in_CReals/Archimedes.con". -inline cic:/CoRN/reals/Q_in_CReals/Archimedes'.con. +inline "cic:/CoRN/reals/Q_in_CReals/Archimedes'.con". (*#**************************************) +coercion "cic:/matita/CoRN-Decl/reals/Q_in_CReals/nat_of_P.con" 0 (* compounds *). + (* end hide *) (*#* @@ -72,21 +70,21 @@ inline cic:/CoRN/reals/Q_in_CReals/Archimedes'.con. To define the injection we need one elemntary lemma about the denominator: *) -inline cic:/CoRN/reals/Q_in_CReals/den_is_nonzero.con. +inline "cic:/CoRN/reals/Q_in_CReals/den_is_nonzero.con". (*#* 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 cic:/CoRN/reals/Q_in_CReals/inj_Q.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q.con". (*#* Next we need some properties of [nring], on the setoid of natural numbers: *) -inline cic:/CoRN/reals/Q_in_CReals/nring_strext.con. +inline "cic:/CoRN/reals/Q_in_CReals/nring_strext.con". -inline cic:/CoRN/reals/Q_in_CReals/nring_wd.con. +inline "cic:/CoRN/reals/Q_in_CReals/nring_wd.con". -inline cic:/CoRN/reals/Q_in_CReals/nring_eq.con. +inline "cic:/CoRN/reals/Q_in_CReals/nring_eq.con". -inline cic:/CoRN/reals/Q_in_CReals/nring_leEq.con. +inline "cic:/CoRN/reals/Q_in_CReals/nring_leEq.con". (* begin hide *) @@ -98,53 +96,53 @@ Unset Printing Coercions. (*#* Similarly we prove some properties of [zring] on the ring of integers: *) -inline cic:/CoRN/reals/Q_in_CReals/zring_strext.con. +inline "cic:/CoRN/reals/Q_in_CReals/zring_strext.con". -inline cic:/CoRN/reals/Q_in_CReals/zring_wd.con. +inline "cic:/CoRN/reals/Q_in_CReals/zring_wd.con". -inline cic:/CoRN/reals/Q_in_CReals/zring_less.con. +inline "cic:/CoRN/reals/Q_in_CReals/zring_less.con". (*#* 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 cic:/CoRN/reals/Q_in_CReals/inj_Q_strext.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_strext.con". -inline cic:/CoRN/reals/Q_in_CReals/inj_Q_wd.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_wd.con". -inline cic:/CoRN/reals/Q_in_CReals/inj_Q_plus.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_plus.con". -inline cic:/CoRN/reals/Q_in_CReals/inj_Q_mult.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_mult.con". -inline cic:/CoRN/reals/Q_in_CReals/inj_Q_less.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_less.con". -inline cic:/CoRN/reals/Q_in_CReals/less_inj_Q.con. +inline "cic:/CoRN/reals/Q_in_CReals/less_inj_Q.con". -inline cic:/CoRN/reals/Q_in_CReals/leEq_inj_Q.con. +inline "cic:/CoRN/reals/Q_in_CReals/leEq_inj_Q.con". -inline cic:/CoRN/reals/Q_in_CReals/inj_Q_leEq.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_leEq.con". -inline cic:/CoRN/reals/Q_in_CReals/inj_Q_min.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_min.con". -inline cic:/CoRN/reals/Q_in_CReals/inj_Q_minus.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_minus.con". (*#* Moreover, and as expected, the [AbsSmall] predicate is also preserved under the [inj_Q] *) -inline cic:/CoRN/reals/Q_in_CReals/inj_Q_AbsSmall.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_AbsSmall.con". -inline cic:/CoRN/reals/Q_in_CReals/AbsSmall_inj_Q.con. +inline "cic:/CoRN/reals/Q_in_CReals/AbsSmall_inj_Q.con". (*#* ** 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 cic:/CoRN/reals/Q_in_CReals/inj_Q_Cauchy.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_Cauchy.con". (*#* 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 cic:/CoRN/reals/Q_in_CReals/inj_Q_nring.con. +inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_nring.con". (*#* ** Injection of [Q] is dense Finally we are able to prove the density of image of [Q] in [R1]. We @@ -157,14 +155,14 @@ because it can be used as an starting point for the typical "interval trisection" argument, which is ubiquitous in constructive analysis. *) -inline cic:/CoRN/reals/Q_in_CReals/start_of_sequence.con. +inline "cic:/CoRN/reals/Q_in_CReals/start_of_sequence.con". (*#* 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 cic:/CoRN/reals/Q_in_CReals/Q_dense_in_CReals.con. +inline "cic:/CoRN/reals/Q_in_CReals/Q_dense_in_CReals.con". (* UNEXPORTED End Rational_sequence_prelogue.