X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCauchy_COF.ma;fp=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCauchy_COF.ma;h=bbf6cda597e8b51909b0ef8b3ba82052b137e77f;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma b/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma new file mode 100644 index 000000000..bbf6cda59 --- /dev/null +++ b/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma @@ -0,0 +1,244 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +include "CoRN.ma". + +(* $Id: Cauchy_COF.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *) + +include "algebra/COrdCauchy.ma". + +include "tactics/RingReflection.ma". + +(*#* +* 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 +*) + +alias id "F" = "cic:/CoRN/algebra/Cauchy_COF/Structure/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 +*) +