matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/Cauchy_COF".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: Cauchy_COF.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
  22
  23 include "algebra/COrdCauchy.ma".
  24
  25 include "tactics/RingReflection.ma".
  26
  27 (*#*
  28 * The Field of Cauchy Sequences
  29
  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].
  32
  33 %\begin{convention}% Let [F] be an ordered field.
  34 %\end{convention}%
  35 *)
  36
  37 (* UNEXPORTED
  38 Section Structure
  39 *)
  40
  41 alias id "F" = "cic:/CoRN/algebra/Cauchy_COF/Structure/F.var".
  42
  43 (*#*
  44 ** Setoid Structure
  45
  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.
  51 *)
  52
  53 inline "cic:/CoRN/algebra/Cauchy_COF/R_Set.con".
  54
  55 (* UNEXPORTED
  56 Section CSetoid_Structure
  57 *)
  58
  59 inline "cic:/CoRN/algebra/Cauchy_COF/R_lt.con".
  60
  61 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap.con".
  62
  63 inline "cic:/CoRN/algebra/Cauchy_COF/R_eq.con".
  64
  65 inline "cic:/CoRN/algebra/Cauchy_COF/R_lt_cotrans.con".
  66
  67 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_cotrans.con".
  68
  69 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_symmetric.con".
  70
  71 inline "cic:/CoRN/algebra/Cauchy_COF/R_lt_irreflexive.con".
  72
  73 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_irreflexive.con".
  74
  75 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_eq_tight.con".
  76
  77 inline "cic:/CoRN/algebra/Cauchy_COF/R_CSetoid.con".
  78
  79 (* UNEXPORTED
  80 End CSetoid_Structure
  81 *)
  82
  83 (* UNEXPORTED
  84 Section Group_Structure
  85 *)
  86
  87 (*#*
  88 ** 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.
  91 *)
  92
  93 inline "cic:/CoRN/algebra/Cauchy_COF/R_plus.con".
  94
  95 inline "cic:/CoRN/algebra/Cauchy_COF/R_zero.con".
  96
  97 inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_lft_ext.con".
  98
  99 inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_assoc.con".
 100
 101 inline "cic:/CoRN/algebra/Cauchy_COF/R_zero_lft_unit.con".
 102
 103 inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_comm.con".
 104
 105 inline "cic:/CoRN/algebra/Cauchy_COF/R_inv.con".
 106
 107 inline "cic:/CoRN/algebra/Cauchy_COF/R_inv_is_inv.con".
 108
 109 inline "cic:/CoRN/algebra/Cauchy_COF/R_inv_ext.con".
 110
 111 inline "cic:/CoRN/algebra/Cauchy_COF/Rinv.con".
 112
 113 inline "cic:/CoRN/algebra/Cauchy_COF/R_CAbGroup.con".
 114
 115 (* UNEXPORTED
 116 End Group_Structure
 117 *)
 118
 119 (* UNEXPORTED
 120 Section Ring_Structure
 121 *)
 122
 123 (*#* ** Ring Structure
 124 Same comments as previously.
 125 *)
 126
 127 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult.con".
 128
 129 inline "cic:/CoRN/algebra/Cauchy_COF/R_one.con".
 130
 131 inline "cic:/CoRN/algebra/Cauchy_COF/R_one_ap_zero.con".
 132
 133 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_plus.con".
 134
 135 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_minus.con".
 136
 137 inline "cic:/CoRN/algebra/Cauchy_COF/R_one_rht_unit.con".
 138
 139 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_comm.con".
 140
 141 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_ap_zero'.con".
 142
 143 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_lft_ext.con".
 144
 145 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_rht_ext.con".
 146
 147 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_strext.con".
 148
 149 inline "cic:/CoRN/algebra/Cauchy_COF/Rmult.con".
 150
 151 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_assoc.con".
 152
 153 inline "cic:/CoRN/algebra/Cauchy_COF/R_one_lft_unit.con".
 154
 155 inline "cic:/CoRN/algebra/Cauchy_COF/R_CRing.con".
 156
 157 (* UNEXPORTED
 158 End Ring_Structure
 159 *)
 160
 161 (* UNEXPORTED
 162 Section Field_Structure
 163 *)
 164
 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.
 169 *)
 170
 171 inline "cic:/CoRN/algebra/Cauchy_COF/R_integral_domain.con".
 172
 173 inline "cic:/CoRN/algebra/Cauchy_COF/R_recip.con".
 174
 175 inline "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse.con".
 176
 177 inline "cic:/CoRN/algebra/Cauchy_COF/R_recip_strext.con".
 178
 179 inline "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse'.con".
 180
 181 inline "cic:/CoRN/algebra/Cauchy_COF/R_CField.con".
 182
 183 (* UNEXPORTED
 184 End Field_Structure
 185 *)
 186
 187 (* UNEXPORTED
 188 Section Order
 189 *)
 190
 191 (*#* ** Order Structure
 192 Finally, we extend the field structure with the ordering we
 193 defined at the beginning.
 194 *)
 195
 196 inline "cic:/CoRN/algebra/Cauchy_COF/R_lt_strext.con".
 197
 198 inline "cic:/CoRN/algebra/Cauchy_COF/Rlt.con".
 199
 200 inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_transitive.con".
 201
 202 inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_strict.con".
 203
 204 inline "cic:/CoRN/algebra/Cauchy_COF/R_plus_resp_lt.con".
 205
 206 inline "cic:/CoRN/algebra/Cauchy_COF/R_mult_resp_lt.con".
 207
 208 inline "cic:/CoRN/algebra/Cauchy_COF/R_COrdField.con".
 209
 210 (* UNEXPORTED
 211 End Order
 212 *)
 213
 214 (*#*
 215 ** Other Results
 216 Auxiliary characterizations of the main relations on [R_Set].
 217 *)
 218
 219 (* UNEXPORTED
 220 Section Auxiliary
 221 *)
 222
 223 inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_1.con".
 224
 225 inline "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_2.con".
 226
 227 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_1.con".
 228
 229 inline "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_1.con".
 230
 231 inline "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_2.con".
 232
 233 inline "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_1.con".
 234
 235 inline "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_2.con".
 236
 237 (* UNEXPORTED
 238 End Auxiliary
 239 *)
 240
 241 (* UNEXPORTED
 242 End Structure
 243 *)
 244