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 *********************)
19 (* $Id: Cauchy_COF.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
21 include "algebra/COrdCauchy.ma".
23 include "tactics/RingReflection.ma".
26 * The Field of Cauchy Sequences
28 In this chapter we will prove that whenever we start from an ordered
29 field [F], we can define a new ordered field of Cauchy sequences over [F].
31 %\begin{convention}% Let [F] be an ordered field.
40 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 procedural "cic:/CoRN/algebra/Cauchy_COF/R_Set.con" as definition.
56 Section CSetoid_Structure
59 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt.con" as definition.
61 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap.con" as definition.
63 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_eq.con" as definition.
65 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt_cotrans.con" as lemma.
67 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_cotrans.con" as lemma.
69 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_symmetric.con" as lemma.
71 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt_irreflexive.con" as lemma.
73 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_irreflexive.con" as lemma.
75 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_eq_tight.con" as lemma.
77 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CSetoid.con" as definition.
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 procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus.con" as definition.
95 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_zero.con" as definition.
97 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_lft_ext.con" as lemma.
99 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_assoc.con" as lemma.
101 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_zero_lft_unit.con" as lemma.
103 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_comm.con" as lemma.
105 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_inv.con" as definition.
107 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_inv_is_inv.con" as lemma.
109 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_inv_ext.con" as lemma.
111 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rinv.con" as definition.
113 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CAbGroup.con" as definition.
120 Section Ring_Structure
123 (*#* ** Ring Structure
124 Same comments as previously.
127 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult.con" as definition.
129 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one.con" as definition.
131 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one_ap_zero.con" as lemma.
133 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_plus.con" as lemma.
135 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_minus.con" as lemma.
137 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one_rht_unit.con" as lemma.
139 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_comm.con" as lemma.
141 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_ap_zero'.con" as lemma.
143 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_lft_ext.con" as lemma.
145 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_rht_ext.con" as lemma.
147 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_strext.con" as lemma.
149 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rmult.con" as definition.
151 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_assoc.con" as lemma.
153 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one_lft_unit.con" as lemma.
155 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CRing.con" as definition.
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 procedural "cic:/CoRN/algebra/Cauchy_COF/R_integral_domain.con" as lemma.
173 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip.con" as definition.
175 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse.con" as lemma.
177 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip_strext.con" as lemma.
179 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse'.con" as lemma.
181 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CField.con" as definition.
191 (*#* ** Order Structure
192 Finally, we extend the field structure with the ordering we
193 defined at the beginning.
196 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt_strext.con" as lemma.
198 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt.con" as definition.
200 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_transitive.con" as lemma.
202 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_strict.con" as lemma.
204 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_resp_lt.con" as lemma.
206 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_resp_lt.con" as lemma.
208 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_COrdField.con" as definition.
216 Auxiliary characterizations of the main relations on [R_Set].
223 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_1.con" as lemma.
225 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_2.con" as lemma.
227 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_1.con" as lemma.
229 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_1.con" as lemma.
231 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_2.con" as lemma.
233 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_1.con" as lemma.
235 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_2.con" as lemma.