1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/Cauchy_COF".
21 (* $Id: Cauchy_COF.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
23 include "algebra/COrdCauchy.ma".
25 include "tactics/RingReflection.ma".
28 * The Field of Cauchy Sequences
30 In this chapter we will prove that whenever we start from an ordered
31 field [F], we can define a new ordered field of Cauchy sequences over [F].
33 %\begin{convention}% Let [F] be an ordered field.
41 alias id "F" = "cic:/CoRN/algebra/Cauchy_COF/Structure/F.var".
46 [R_Set] is the setoid of Cauchy sequences over [F]; given two sequences
47 [x,y] over [F], we say that [x] is smaller than [y] if from some point
48 onwards [(y n) [-] (x n)] is greater than some fixed, positive
49 [e]. Apartness of two sequences means that one of them is smaller
50 than the other, equality is the negation of the apartness.
53 inline "cic:/CoRN/algebra/Cauchy_COF/R_Set.con".
56 Section CSetoid_Structure
59 inline "cic:/CoRN/algebra/Cauchy_COF/R_lt.con".
61 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap.con".
63 inline "cic:/CoRN/algebra/Cauchy_COF/R_eq.con".
65 inline "cic:/CoRN/algebra/Cauchy_COF/R_lt_cotrans.con".
67 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_cotrans.con".
69 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_symmetric.con".
71 inline "cic:/CoRN/algebra/Cauchy_COF/R_lt_irreflexive.con".
73 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_irreflexive.con".
75 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_eq_tight.con".
77 inline "cic:/CoRN/algebra/Cauchy_COF/R_CSetoid.con".
84 Section Group_Structure
89 The group structure is just the expected one; the lemmas which
90 are specifically proved are just the necessary ones to get the group axioms.
93 inline "cic:/CoRN/algebra/Cauchy_COF/R_plus.con".
95 inline "cic:/CoRN/algebra/Cauchy_COF/R_zero.con".
97 inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_lft_ext.con".
99 inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_assoc.con".
101 inline "cic:/CoRN/algebra/Cauchy_COF/R_zero_lft_unit.con".
103 inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_comm.con".
105 inline "cic:/CoRN/algebra/Cauchy_COF/R_inv.con".
107 inline "cic:/CoRN/algebra/Cauchy_COF/R_inv_is_inv.con".
109 inline "cic:/CoRN/algebra/Cauchy_COF/R_inv_ext.con".
111 inline "cic:/CoRN/algebra/Cauchy_COF/Rinv.con".
113 inline "cic:/CoRN/algebra/Cauchy_COF/R_CAbGroup.con".
120 Section Ring_Structure
123 (*#* ** Ring Structure
124 Same comments as previously.
127 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult.con".
129 inline "cic:/CoRN/algebra/Cauchy_COF/R_one.con".
131 inline "cic:/CoRN/algebra/Cauchy_COF/R_one_ap_zero.con".
133 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_plus.con".
135 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_minus.con".
137 inline "cic:/CoRN/algebra/Cauchy_COF/R_one_rht_unit.con".
139 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_comm.con".
141 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_ap_zero'.con".
143 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_lft_ext.con".
145 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_rht_ext.con".
147 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_strext.con".
149 inline "cic:/CoRN/algebra/Cauchy_COF/Rmult.con".
151 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_assoc.con".
153 inline "cic:/CoRN/algebra/Cauchy_COF/R_one_lft_unit.con".
155 inline "cic:/CoRN/algebra/Cauchy_COF/R_CRing.con".
162 Section Field_Structure
165 (*#* ** Field Structure
166 For the field structure, it is technically easier to first prove
167 that our ring is actually an integral domain. The rest then follows
168 quite straightforwardly.
171 inline "cic:/CoRN/algebra/Cauchy_COF/R_integral_domain.con".
173 inline "cic:/CoRN/algebra/Cauchy_COF/R_recip.con".
175 inline "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse.con".
177 inline "cic:/CoRN/algebra/Cauchy_COF/R_recip_strext.con".
179 inline "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse'.con".
181 inline "cic:/CoRN/algebra/Cauchy_COF/R_CField.con".
191 (*#* ** Order Structure
192 Finally, we extend the field structure with the ordering we
193 defined at the beginning.
196 inline "cic:/CoRN/algebra/Cauchy_COF/R_lt_strext.con".
198 inline "cic:/CoRN/algebra/Cauchy_COF/Rlt.con".
200 inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_transitive.con".
202 inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_strict.con".
204 inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_resp_lt.con".
206 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_resp_lt.con".
208 inline "cic:/CoRN/algebra/Cauchy_COF/R_COrdField.con".
216 Auxiliary characterizations of the main relations on [R_Set].
223 inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_1.con".
225 inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_2.con".
227 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_1.con".
229 inline "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_1.con".
231 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_2.con".
233 inline "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_1.con".
235 inline "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_2.con".