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 *********************)
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. *)
25 include "reals/CReals.ma".
27 (* This comes from CReals1.v *)
29 inline procedural "cic:/CoRN/reals/R_morphism/Cauchy_Lim_prop2.con" as definition.
36 cic:/CoRN/reals/R_morphism/morphism/R1.var
40 cic:/CoRN/reals/R_morphism/morphism/R2.var
44 Section morphism_details
48 cic:/CoRN/reals/R_morphism/morphism/morphism_details/phi.var
52 cic:/CoRN/reals/R_morphism/morphism/morphism_details/p1.var
56 cic:/CoRN/reals/R_morphism/morphism/morphism_details/p2.var
60 cic:/CoRN/reals/R_morphism/morphism/morphism_details/f1.var
64 cic:/CoRN/reals/R_morphism/morphism/morphism_details/f2.var
68 cic:/CoRN/reals/R_morphism/morphism/morphism_details/g1.var
72 cic:/CoRN/reals/R_morphism/morphism/morphism_details/g2.var
75 inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_relation.con" as definition.
77 inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_un_fun.con" as definition.
79 inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_bin_fun.con" as definition.
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))).
86 inline procedural "cic:/CoRN/reals/R_morphism/fun_pres_Lim.con" as definition.
92 inline procedural "cic:/CoRN/reals/R_morphism/Homomorphism.ind".
95 cic:/matita/CoRN-Procedural/reals/R_morphism/map.con
98 (* This might be useful later...
99 Definition Homo_as_CSetoid_fun:=
101 (Build_CSetoid_fun R1 R2 f
102 (fun_strext_imp_wd R1 R2 f (!map_strext f))
107 inline procedural "cic:/CoRN/reals/R_morphism/map_strext_unfolded.con" as lemma.
109 inline procedural "cic:/CoRN/reals/R_morphism/map_wd_unfolded.con" as lemma.
111 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_less_unfolded.con" as lemma.
113 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_plus_unfolded.con" as lemma.
115 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_mult_unfolded.con" as lemma.
117 (* Now we start to derive some useful properties of a Homomorphism *)
119 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_zero.con" as lemma.
121 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_zero_unfolded.con" as lemma.
123 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_minus.con" as lemma.
125 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_minus_unfolded.con" as lemma.
127 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_apartness.con" as lemma.
129 (* Merely a useful special case *)
131 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_ap_zero.con" as lemma.
133 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_one.con" as lemma.
135 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_one_unfolded.con" as lemma.
137 (* I will not use the following lemma *)
139 inline procedural "cic:/CoRN/reals/R_morphism/map_pres_inv_unfolded.con" as lemma.
150 cic:/CoRN/reals/R_morphism/composition/R1.var
154 cic:/CoRN/reals/R_morphism/composition/R2.var
158 cic:/CoRN/reals/R_morphism/composition/R3.var
162 cic:/CoRN/reals/R_morphism/composition/f.var
166 cic:/CoRN/reals/R_morphism/composition/g.var
169 inline procedural "cic:/CoRN/reals/R_morphism/compose.con" as definition.
171 inline procedural "cic:/CoRN/reals/R_morphism/compose_strext.con" as lemma.
173 inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_less.con" as lemma.
175 inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_plus.con" as lemma.
177 inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_mult.con" as lemma.
179 inline procedural "cic:/CoRN/reals/R_morphism/compose_pres_Lim.con" as lemma.
181 inline procedural "cic:/CoRN/reals/R_morphism/Compose.con" as definition.
192 cic:/CoRN/reals/R_morphism/isomorphism/R1.var
196 cic:/CoRN/reals/R_morphism/isomorphism/R2.var
204 cic:/CoRN/reals/R_morphism/isomorphism/identity_map/R3.var
208 cic:/CoRN/reals/R_morphism/isomorphism/identity_map/f.var
211 inline procedural "cic:/CoRN/reals/R_morphism/map_is_id.con" as definition.
217 inline procedural "cic:/CoRN/reals/R_morphism/Isomorphism.ind".
224 Section surjective_map
228 cic:/CoRN/reals/R_morphism/surjective_map/R1.var
232 cic:/CoRN/reals/R_morphism/surjective_map/R2.var
236 cic:/CoRN/reals/R_morphism/surjective_map/f.var
239 inline procedural "cic:/CoRN/reals/R_morphism/map_is_surjective.con" as definition.
246 Section simplification
250 cic:/CoRN/reals/R_morphism/simplification/R1.var
254 cic:/CoRN/reals/R_morphism/simplification/R2.var
258 cic:/CoRN/reals/R_morphism/simplification/f.var
262 cic:/CoRN/reals/R_morphism/simplification/H1.var
265 inline procedural "cic:/CoRN/reals/R_morphism/f_well_def.con" as lemma.
272 cic:/CoRN/reals/R_morphism/simplification/with_less/H2.var
275 inline procedural "cic:/CoRN/reals/R_morphism/less_pres_f.con" as lemma.
277 inline procedural "cic:/CoRN/reals/R_morphism/leEq_pres_f.con" as lemma.
279 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_leEq.con" as lemma.
281 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_apartness.con" as lemma.
292 cic:/CoRN/reals/R_morphism/simplification/with_plus/H3.var
295 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_Zero.con" as lemma.
297 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_minus.con" as lemma.
299 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_min.con" as lemma.
306 Section with_plus_less
310 cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H2.var
314 cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H3.var
317 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_ap_zero.con" as lemma.
320 Section surjectivity_helps
324 cic:/CoRN/reals/R_morphism/simplification/with_plus_less/surjectivity_helps/f_surj.var
327 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_Lim.con" as lemma.
330 End surjectivity_helps
334 Section with_mult_plus_less
338 cic:/CoRN/reals/R_morphism/simplification/with_plus_less/with_mult_plus_less/H4.var
341 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_one.con" as lemma.
343 inline procedural "cic:/CoRN/reals/R_morphism/f_pres_inv.con" as lemma.
345 inline procedural "cic:/CoRN/reals/R_morphism/simplified_Homomorphism.con" as definition.
348 End with_mult_plus_less