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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/reals/R_morphism".
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. *)
27 include "reals/CReals.ma".
29 (* This comes from CReals1.v *)
31 inline "cic:/CoRN/reals/R_morphism/Cauchy_Lim_prop2.con".
37 inline "cic:/CoRN/reals/R_morphism/R1.var".
39 inline "cic:/CoRN/reals/R_morphism/R2.var".
42 Section morphism_details.
45 inline "cic:/CoRN/reals/R_morphism/phi.var".
47 inline "cic:/CoRN/reals/R_morphism/p1.var".
49 inline "cic:/CoRN/reals/R_morphism/p2.var".
51 inline "cic:/CoRN/reals/R_morphism/f1.var".
53 inline "cic:/CoRN/reals/R_morphism/f2.var".
55 inline "cic:/CoRN/reals/R_morphism/g1.var".
57 inline "cic:/CoRN/reals/R_morphism/g2.var".
59 inline "cic:/CoRN/reals/R_morphism/fun_pres_relation.con".
61 inline "cic:/CoRN/reals/R_morphism/fun_pres_un_fun.con".
63 inline "cic:/CoRN/reals/R_morphism/fun_pres_bin_fun.con".
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))).
70 inline "cic:/CoRN/reals/R_morphism/fun_pres_Lim.con".
76 inline "cic:/CoRN/reals/R_morphism/Homomorphism.ind".
78 coercion "cic:/matita/CoRN-Decl/reals/R_morphism/map.con" 0 (* compounds *).
80 (* This might be useful later...
81 Definition Homo_as_CSetoid_fun:=
83 (Build_CSetoid_fun R1 R2 f
84 (fun_strext_imp_wd R1 R2 f (!map_strext f))
89 inline "cic:/CoRN/reals/R_morphism/map_strext_unfolded.con".
91 inline "cic:/CoRN/reals/R_morphism/map_wd_unfolded.con".
93 inline "cic:/CoRN/reals/R_morphism/map_pres_less_unfolded.con".
95 inline "cic:/CoRN/reals/R_morphism/map_pres_plus_unfolded.con".
97 inline "cic:/CoRN/reals/R_morphism/map_pres_mult_unfolded.con".
99 (* Now we start to derive some useful properties of a Homomorphism *)
101 inline "cic:/CoRN/reals/R_morphism/map_pres_zero.con".
103 inline "cic:/CoRN/reals/R_morphism/map_pres_zero_unfolded.con".
105 inline "cic:/CoRN/reals/R_morphism/map_pres_minus.con".
107 inline "cic:/CoRN/reals/R_morphism/map_pres_minus_unfolded.con".
109 inline "cic:/CoRN/reals/R_morphism/map_pres_apartness.con".
111 (* Merely a useful special case *)
113 inline "cic:/CoRN/reals/R_morphism/map_pres_ap_zero.con".
115 inline "cic:/CoRN/reals/R_morphism/map_pres_one.con".
117 inline "cic:/CoRN/reals/R_morphism/map_pres_one_unfolded.con".
119 (* I will not use the following lemma *)
121 inline "cic:/CoRN/reals/R_morphism/map_pres_inv_unfolded.con".
131 inline "cic:/CoRN/reals/R_morphism/R1.var".
133 inline "cic:/CoRN/reals/R_morphism/R2.var".
135 inline "cic:/CoRN/reals/R_morphism/R3.var".
137 inline "cic:/CoRN/reals/R_morphism/f.var".
139 inline "cic:/CoRN/reals/R_morphism/g.var".
141 inline "cic:/CoRN/reals/R_morphism/compose.con".
143 inline "cic:/CoRN/reals/R_morphism/compose_strext.con".
145 inline "cic:/CoRN/reals/R_morphism/compose_pres_less.con".
147 inline "cic:/CoRN/reals/R_morphism/compose_pres_plus.con".
149 inline "cic:/CoRN/reals/R_morphism/compose_pres_mult.con".
151 inline "cic:/CoRN/reals/R_morphism/compose_pres_Lim.con".
153 inline "cic:/CoRN/reals/R_morphism/Compose.con".
163 inline "cic:/CoRN/reals/R_morphism/R1.var".
165 inline "cic:/CoRN/reals/R_morphism/R2.var".
168 Section identity_map.
171 inline "cic:/CoRN/reals/R_morphism/R3.var".
173 inline "cic:/CoRN/reals/R_morphism/f.var".
175 inline "cic:/CoRN/reals/R_morphism/map_is_id.con".
181 inline "cic:/CoRN/reals/R_morphism/Isomorphism.ind".
188 Section surjective_map.
191 inline "cic:/CoRN/reals/R_morphism/R1.var".
193 inline "cic:/CoRN/reals/R_morphism/R2.var".
195 inline "cic:/CoRN/reals/R_morphism/f.var".
197 inline "cic:/CoRN/reals/R_morphism/map_is_surjective.con".
204 Section simplification.
207 inline "cic:/CoRN/reals/R_morphism/R1.var".
209 inline "cic:/CoRN/reals/R_morphism/R2.var".
211 inline "cic:/CoRN/reals/R_morphism/f.var".
213 inline "cic:/CoRN/reals/R_morphism/H1.var".
215 inline "cic:/CoRN/reals/R_morphism/f_well_def.con".
221 inline "cic:/CoRN/reals/R_morphism/H2.var".
223 inline "cic:/CoRN/reals/R_morphism/less_pres_f.con".
225 inline "cic:/CoRN/reals/R_morphism/leEq_pres_f.con".
227 inline "cic:/CoRN/reals/R_morphism/f_pres_leEq.con".
229 inline "cic:/CoRN/reals/R_morphism/f_pres_apartness.con".
239 inline "cic:/CoRN/reals/R_morphism/H3.var".
241 inline "cic:/CoRN/reals/R_morphism/f_pres_Zero.con".
243 inline "cic:/CoRN/reals/R_morphism/f_pres_minus.con".
245 inline "cic:/CoRN/reals/R_morphism/f_pres_min.con".
252 Section with_plus_less.
255 inline "cic:/CoRN/reals/R_morphism/H2.var".
257 inline "cic:/CoRN/reals/R_morphism/H3.var".
259 inline "cic:/CoRN/reals/R_morphism/f_pres_ap_zero.con".
262 Section surjectivity_helps.
265 inline "cic:/CoRN/reals/R_morphism/f_surj.var".
267 inline "cic:/CoRN/reals/R_morphism/f_pres_Lim.con".
270 End surjectivity_helps.
274 Section with_mult_plus_less.
277 inline "cic:/CoRN/reals/R_morphism/H4.var".
279 inline "cic:/CoRN/reals/R_morphism/f_pres_one.con".
281 inline "cic:/CoRN/reals/R_morphism/f_pres_inv.con".
283 inline "cic:/CoRN/reals/R_morphism/simplified_Homomorphism.con".
286 End with_mult_plus_less.