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