(**************************************************************************) (* ___ *) (* ||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 *********************) 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 *) (* UNEXPORTED 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 procedural "cic:/CoRN/algebra/Cauchy_COF/R_Set.con" as definition. (* UNEXPORTED Section CSetoid_Structure *) inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_eq.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt_cotrans.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_cotrans.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_symmetric.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt_irreflexive.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_irreflexive.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_eq_tight.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CSetoid.con" as definition. (* 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 procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_zero.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_lft_ext.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_assoc.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_zero_lft_unit.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_comm.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_inv.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_inv_is_inv.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_inv_ext.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rinv.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CAbGroup.con" as definition. (* UNEXPORTED End Group_Structure *) (* UNEXPORTED Section Ring_Structure *) (*#* ** Ring Structure Same comments as previously. *) inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one_ap_zero.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_plus.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_minus.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one_rht_unit.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_comm.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_ap_zero'.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_lft_ext.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_rht_ext.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_strext.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rmult.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_assoc.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one_lft_unit.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CRing.con" as definition. (* 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 procedural "cic:/CoRN/algebra/Cauchy_COF/R_integral_domain.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip_strext.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse'.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CField.con" as definition. (* UNEXPORTED End Field_Structure *) (* UNEXPORTED Section Order *) (*#* ** Order Structure Finally, we extend the field structure with the ordering we defined at the beginning. *) inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt_strext.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt.con" as definition. inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_transitive.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_strict.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_resp_lt.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_resp_lt.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_COrdField.con" as definition. (* UNEXPORTED End Order *) (*#* ** Other Results Auxiliary characterizations of the main relations on [R_Set]. *) (* UNEXPORTED Section Auxiliary *) inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_1.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_2.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_1.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_1.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_2.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_1.con" as lemma. inline procedural "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_2.con" as lemma. (* UNEXPORTED End Auxiliary *) (* UNEXPORTED End Structure *)