--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+*)
+
projects / helm.git / blobdiff