helm/software/matita/contribs/procedural/CoRN/reals/R_morphism.mma

   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 include "CoRN.ma".
  18
  19 (* begin hide *)
  20
  21 (* In this file a notion of morphism between two arbitrary real number
  22    structures, is introduced together with te proofs that this notion of
  23    morphism preserves the basic algebraic structure. *)
  24
  25 include "reals/CReals.ma".
  26
  27 (* This comes from CReals1.v *)
  28
  29 inline procedural "cic:/CoRN/reals/R_morphism/Cauchy_Lim_prop2.con" as definition.
  30
  31 (* UNEXPORTED
  32 Section morphism
  33 *)
  34
  35 (* UNEXPORTED
  36 cic:/CoRN/reals/R_morphism/morphism/R1.var
  37 *)
  38
  39 (* UNEXPORTED
  40 cic:/CoRN/reals/R_morphism/morphism/R2.var
  41 *)
  42
  43 (* UNEXPORTED
  44 Section morphism_details
  45 *)
  46
  47 (* UNEXPORTED
  48 cic:/CoRN/reals/R_morphism/morphism/morphism_details/phi.var
  49 *)
  50
  51 (* UNEXPORTED
  52 cic:/CoRN/reals/R_morphism/morphism/morphism_details/p1.var
  53 *)
  54
  55 (* UNEXPORTED
  56 cic:/CoRN/reals/R_morphism/morphism/morphism_details/p2.var
  57 *)
  58
  59 (* UNEXPORTED
  60 cic:/CoRN/reals/R_morphism/morphism/morphism_details/f1.var
  61 *)
  62
  63 (* UNEXPORTED
  64 cic:/CoRN/reals/R_morphism/morphism/morphism_details/f2.var
  65 *)
  66
  67 (* UNEXPORTED
  68 cic:/CoRN/reals/R_morphism/morphism/morphism_details/g1.var
  69 *)
  70
  71 (* UNEXPORTED
  72 cic:/CoRN/reals/R_morphism/morphism/morphism_details/g2.var
  73 *)
  74
  75 inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_relation.con" as definition.
  76
  77 inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_un_fun.con" as definition.
  78
  79 inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_bin_fun.con" as definition.
  80
  81 (*
  82 Definition fun_pres_partial_fun:=(x:R1;H1:x[#]Zero;H2:(phi x)[#]Zero)
  83 (phi (nzinj R1 (i1 (nzpro R1 x H1))))[=](nzinj R2 (i2 (nzpro R2 (phi x) H2))).
  84 *)
  85
  86 inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_Lim.con" as definition.
  87
  88 (* UNEXPORTED
  89 End morphism_details
  90 *)
  91
  92 inline procedural "cic:/CoRN/reals/R_morphism/Homomorphism.ind".
  93
  94 (* COERCION
  95 cic:/matita/CoRN-Procedural/reals/R_morphism/map.con
  96 *)
  97
  98 (* This might be useful later...
  99 Definition Homo_as_CSetoid_fun:=
 100     [f:Homomorphism]
 101          (Build_CSetoid_fun R1 R2 f
 102            (fun_strext_imp_wd R1 R2 f (!map_strext f))
 103            (!map_strext f)
 104           ).
 105 *****************)
 106
 107 inline procedural "cic:/CoRN/reals/R_morphism/map_strext_unfolded.con" as lemma.
 108
 109 inline procedural "cic:/CoRN/reals/R_morphism/map_wd_unfolded.con" as lemma.
 110
 111 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_less_unfolded.con" as lemma.
 112
 113 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_plus_unfolded.con" as lemma.
 114
 115 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_mult_unfolded.con" as lemma.
 116
 117 (* Now we start to derive some useful properties of a Homomorphism *)
 118
 119 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_zero.con" as lemma.
 120
 121 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_zero_unfolded.con" as lemma.
 122
 123 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_minus.con" as lemma.
 124
 125 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_minus_unfolded.con" as lemma.
 126
 127 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_apartness.con" as lemma.
 128
 129 (* Merely a useful special case *)
 130
 131 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_ap_zero.con" as lemma.
 132
 133 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_one.con" as lemma.
 134
 135 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_one_unfolded.con" as lemma.
 136
 137 (* I will not use the following lemma *)
 138
 139 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_inv_unfolded.con" as lemma.
 140
 141 (* UNEXPORTED
 142 End morphism
 143 *)
 144
 145 (* UNEXPORTED
 146 Section composition
 147 *)
 148
 149 (* UNEXPORTED
 150 cic:/CoRN/reals/R_morphism/composition/R1.var
 151 *)
 152
 153 (* UNEXPORTED
 154 cic:/CoRN/reals/R_morphism/composition/R2.var
 155 *)
 156
 157 (* UNEXPORTED
 158 cic:/CoRN/reals/R_morphism/composition/R3.var
 159 *)
 160
 161 (* UNEXPORTED
 162 cic:/CoRN/reals/R_morphism/composition/f.var
 163 *)
 164
 165 (* UNEXPORTED
 166 cic:/CoRN/reals/R_morphism/composition/g.var
 167 *)
 168
 169 inline procedural "cic:/CoRN/reals/R_morphism/compose.con" as definition.
 170
 171 inline procedural "cic:/CoRN/reals/R_morphism/compose_strext.con" as lemma.
 172
 173 inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_less.con" as lemma.
 174
 175 inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_plus.con" as lemma.
 176
 177 inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_mult.con" as lemma.
 178
 179 inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_Lim.con" as lemma.
 180
 181 inline procedural "cic:/CoRN/reals/R_morphism/Compose.con" as definition.
 182
 183 (* UNEXPORTED
 184 End composition
 185 *)
 186
 187 (* UNEXPORTED
 188 Section isomorphism
 189 *)
 190
 191 (* UNEXPORTED
 192 cic:/CoRN/reals/R_morphism/isomorphism/R1.var
 193 *)
 194
 195 (* UNEXPORTED
 196 cic:/CoRN/reals/R_morphism/isomorphism/R2.var
 197 *)
 198
 199 (* UNEXPORTED
 200 Section identity_map
 201 *)
 202
 203 (* UNEXPORTED
 204 cic:/CoRN/reals/R_morphism/isomorphism/identity_map/R3.var
 205 *)
 206
 207 (* UNEXPORTED
 208 cic:/CoRN/reals/R_morphism/isomorphism/identity_map/f.var
 209 *)
 210
 211 inline procedural "cic:/CoRN/reals/R_morphism/map_is_id.con" as definition.
 212
 213 (* UNEXPORTED
 214 End identity_map
 215 *)
 216
 217 inline procedural "cic:/CoRN/reals/R_morphism/Isomorphism.ind".
 218
 219 (* UNEXPORTED
 220 End isomorphism
 221 *)
 222
 223 (* UNEXPORTED
 224 Section surjective_map
 225 *)
 226
 227 (* UNEXPORTED
 228 cic:/CoRN/reals/R_morphism/surjective_map/R1.var
 229 *)
 230
 231 (* UNEXPORTED
 232 cic:/CoRN/reals/R_morphism/surjective_map/R2.var
 233 *)
 234
 235 (* UNEXPORTED
 236 cic:/CoRN/reals/R_morphism/surjective_map/f.var
 237 *)
 238
 239 inline procedural "cic:/CoRN/reals/R_morphism/map_is_surjective.con" as definition.
 240
 241 (* UNEXPORTED
 242 End surjective_map
 243 *)
 244
 245 (* UNEXPORTED
 246 Section simplification
 247 *)
 248
 249 (* UNEXPORTED
 250 cic:/CoRN/reals/R_morphism/simplification/R1.var
 251 *)
 252
 253 (* UNEXPORTED
 254 cic:/CoRN/reals/R_morphism/simplification/R2.var
 255 *)
 256
 257 (* UNEXPORTED
 258 cic:/CoRN/reals/R_morphism/simplification/f.var
 259 *)
 260
 261 (* UNEXPORTED
 262 cic:/CoRN/reals/R_morphism/simplification/H1.var
 263 *)
 264
 265 inline procedural "cic:/CoRN/reals/R_morphism/f_well_def.con" as lemma.
 266
 267 (* UNEXPORTED
 268 Section with_less
 269 *)
 270
 271 (* UNEXPORTED
 272 cic:/CoRN/reals/R_morphism/simplification/with_less/H2.var
 273 *)
 274
 275 inline procedural "cic:/CoRN/reals/R_morphism/less_pres_f.con" as lemma.
 276
 277 inline procedural "cic:/CoRN/reals/R_morphism/leEq_pres_f.con" as lemma.
 278
 279 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_leEq.con" as lemma.
 280
 281 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_apartness.con" as lemma.
 282
 283 (* UNEXPORTED
 284 End with_less
 285 *)
 286
 287 (* UNEXPORTED
 288 Section with_plus
 289 *)
 290
 291 (* UNEXPORTED
 292 cic:/CoRN/reals/R_morphism/simplification/with_plus/H3.var
 293 *)
 294
 295 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_Zero.con" as lemma.
 296
 297 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_minus.con" as lemma.
 298
 299 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_min.con" as lemma.
 300
 301 (* UNEXPORTED
 302 End with_plus
 303 *)
 304
 305 (* UNEXPORTED
 306 Section with_plus_less
 307 *)
 308
 309 (* UNEXPORTED
 310 cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H2.var
 311 *)
 312
 313 (* UNEXPORTED
 314 cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H3.var
 315 *)
 316
 317 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_ap_zero.con" as lemma.
 318
 319 (* UNEXPORTED
 320 Section surjectivity_helps
 321 *)
 322
 323 (* UNEXPORTED
 324 cic:/CoRN/reals/R_morphism/simplification/with_plus_less/surjectivity_helps/f_surj.var
 325 *)
 326
 327 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_Lim.con" as lemma.
 328
 329 (* UNEXPORTED
 330 End surjectivity_helps
 331 *)
 332
 333 (* UNEXPORTED
 334 Section with_mult_plus_less
 335 *)
 336
 337 (* UNEXPORTED
 338 cic:/CoRN/reals/R_morphism/simplification/with_plus_less/with_mult_plus_less/H4.var
 339 *)
 340
 341 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_one.con" as lemma.
 342
 343 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_inv.con" as lemma.
 344
 345 inline procedural "cic:/CoRN/reals/R_morphism/simplified_Homomorphism.con" as definition.
 346
 347 (* UNEXPORTED
 348 End with_mult_plus_less
 349 *)
 350
 351 (* UNEXPORTED
 352 End with_plus_less
 353 *)
 354
 355 (* UNEXPORTED
 356 End simplification
 357 *)
 358
 359 (* end hide *)
 360