X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCauchy_COF.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCauchy_COF.ma;h=f2ee13a4916a58d538f4a2087dd2f53a58bf31a9;hb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;hp=0000000000000000000000000000000000000000;hpb=438a29376390222b94c1fe9772917c3aad50d42e;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma new file mode 100644 index 000000000..f2ee13a49 --- /dev/null +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma @@ -0,0 +1,246 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/CoRN-Decl/algebra/Cauchy_COF". + +(* $Id: Cauchy_COF.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *) + +(* INCLUDE +COrdCauchy +*) + +(* INCLUDE +RingReflection +*) + +(*#* +* The Field of Cauchy Sequences + +In this chapter we will prove that whenever we start from an ordered +field [F], we can define a new ordered field of Cauchy sequences over [F]. + +%\begin{convention}% Let [F] be an ordered field. +%\end{convention}% +*) + +(* UNEXPORTED +Section Structure. +*) + +inline cic:/CoRN/algebra/Cauchy_COF/F.var. + +(*#* +** Setoid Structure + +[R_Set] is the setoid of Cauchy sequences over [F]; given two sequences +[x,y] over [F], we say that [x] is smaller than [y] if from some point +onwards [(y n) [-] (x n)] is greater than some fixed, positive +[e]. Apartness of two sequences means that one of them is smaller +than the other, equality is the negation of the apartness. +*) + +inline cic:/CoRN/algebra/Cauchy_COF/R_Set.con. + +(* UNEXPORTED +Section CSetoid_Structure. +*) + +inline cic:/CoRN/algebra/Cauchy_COF/R_lt.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_ap.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_eq.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_lt_cotrans.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_ap_cotrans.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_ap_symmetric.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_lt_irreflexive.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_ap_irreflexive.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_ap_eq_tight.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_CSetoid.con. + +(* UNEXPORTED +End CSetoid_Structure. +*) + +(* UNEXPORTED +Section Group_Structure. +*) + +(*#* +** Group Structure +The group structure is just the expected one; the lemmas which +are specifically proved are just the necessary ones to get the group axioms. +*) + +inline cic:/CoRN/algebra/Cauchy_COF/R_plus.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_zero.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_plus_lft_ext.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_plus_assoc.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_zero_lft_unit.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_plus_comm.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_inv.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_inv_is_inv.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_inv_ext.con. + +inline cic:/CoRN/algebra/Cauchy_COF/Rinv.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_CAbGroup.con. + +(* UNEXPORTED +End Group_Structure. +*) + +(* UNEXPORTED +Section Ring_Structure. +*) + +(*#* ** Ring Structure +Same comments as previously. +*) + +inline cic:/CoRN/algebra/Cauchy_COF/R_mult.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_one.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_one_ap_zero.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_plus.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_minus.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_one_rht_unit.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_mult_comm.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_mult_ap_zero'.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_mult_lft_ext.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_mult_rht_ext.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_mult_strext.con. + +inline cic:/CoRN/algebra/Cauchy_COF/Rmult.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_mult_assoc.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_one_lft_unit.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_CRing.con. + +(* UNEXPORTED +End Ring_Structure. +*) + +(* UNEXPORTED +Section Field_Structure. +*) + +(*#* ** Field Structure +For the field structure, it is technically easier to first prove +that our ring is actually an integral domain. The rest then follows +quite straightforwardly. +*) + +inline cic:/CoRN/algebra/Cauchy_COF/R_integral_domain.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_recip.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_recip_strext.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse'.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_CField.con. + +(* UNEXPORTED +End Field_Structure. +*) + +(* UNEXPORTED +Section Order. +*) + +(*#* ** Order Structure +Finally, we extend the field structure with the ordering we +defined at the beginning. +*) + +inline cic:/CoRN/algebra/Cauchy_COF/R_lt_strext.con. + +inline cic:/CoRN/algebra/Cauchy_COF/Rlt.con. + +inline cic:/CoRN/algebra/Cauchy_COF/Rlt_transitive.con. + +inline cic:/CoRN/algebra/Cauchy_COF/Rlt_strict.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_plus_resp_lt.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_mult_resp_lt.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_COrdField.con. + +(* UNEXPORTED +End Order. +*) + +(*#* +** Other Results +Auxiliary characterizations of the main relations on [R_Set]. +*) + +(* UNEXPORTED +Section Auxiliary. +*) + +inline cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_1.con. + +inline cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_2.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_1.con. + +inline cic:/CoRN/algebra/Cauchy_COF/Eq_alt_1.con. + +inline cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_2.con. + +inline cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_1.con. + +inline cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_2.con. + +(* UNEXPORTED +End Auxiliary. +*) + +(* UNEXPORTED +End Structure. +*) +