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".
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. *)
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 (* This might be useful later...
79 Definition Homo_as_CSetoid_fun:=
81 (Build_CSetoid_fun R1 R2 f
82 (fun_strext_imp_wd R1 R2 f (!map_strext f))
87 inline cic:/CoRN/reals/R_morphism/map_strext_unfolded.con.
89 inline cic:/CoRN/reals/R_morphism/map_wd_unfolded.con.
91 inline cic:/CoRN/reals/R_morphism/map_pres_less_unfolded.con.
93 inline cic:/CoRN/reals/R_morphism/map_pres_plus_unfolded.con.
95 inline cic:/CoRN/reals/R_morphism/map_pres_mult_unfolded.con.
97 (* Now we start to derive some useful properties of a Homomorphism *)
99 inline cic:/CoRN/reals/R_morphism/map_pres_zero.con.
101 inline cic:/CoRN/reals/R_morphism/map_pres_zero_unfolded.con.
103 inline cic:/CoRN/reals/R_morphism/map_pres_minus.con.
105 inline cic:/CoRN/reals/R_morphism/map_pres_minus_unfolded.con.
107 inline cic:/CoRN/reals/R_morphism/map_pres_apartness.con.
109 (* Merely a useful special case *)
111 inline cic:/CoRN/reals/R_morphism/map_pres_ap_zero.con.
113 inline cic:/CoRN/reals/R_morphism/map_pres_one.con.
115 inline cic:/CoRN/reals/R_morphism/map_pres_one_unfolded.con.
117 (* I will not use the following lemma *)
119 inline cic:/CoRN/reals/R_morphism/map_pres_inv_unfolded.con.
129 inline cic:/CoRN/reals/R_morphism/R1.var.
131 inline cic:/CoRN/reals/R_morphism/R2.var.
133 inline cic:/CoRN/reals/R_morphism/R3.var.
135 inline cic:/CoRN/reals/R_morphism/f.var.
137 inline cic:/CoRN/reals/R_morphism/g.var.
139 inline cic:/CoRN/reals/R_morphism/compose.con.
141 inline cic:/CoRN/reals/R_morphism/compose_strext.con.
143 inline cic:/CoRN/reals/R_morphism/compose_pres_less.con.
145 inline cic:/CoRN/reals/R_morphism/compose_pres_plus.con.
147 inline cic:/CoRN/reals/R_morphism/compose_pres_mult.con.
149 inline cic:/CoRN/reals/R_morphism/compose_pres_Lim.con.
151 inline cic:/CoRN/reals/R_morphism/Compose.con.
161 inline cic:/CoRN/reals/R_morphism/R1.var.
163 inline cic:/CoRN/reals/R_morphism/R2.var.
166 Section identity_map.
169 inline cic:/CoRN/reals/R_morphism/R3.var.
171 inline cic:/CoRN/reals/R_morphism/f.var.
173 inline cic:/CoRN/reals/R_morphism/map_is_id.con.
179 inline cic:/CoRN/reals/R_morphism/Isomorphism.ind.
186 Section surjective_map.
189 inline cic:/CoRN/reals/R_morphism/R1.var.
191 inline cic:/CoRN/reals/R_morphism/R2.var.
193 inline cic:/CoRN/reals/R_morphism/f.var.
195 inline cic:/CoRN/reals/R_morphism/map_is_surjective.con.
202 Section simplification.
205 inline cic:/CoRN/reals/R_morphism/R1.var.
207 inline cic:/CoRN/reals/R_morphism/R2.var.
209 inline cic:/CoRN/reals/R_morphism/f.var.
211 inline cic:/CoRN/reals/R_morphism/H1.var.
213 inline cic:/CoRN/reals/R_morphism/f_well_def.con.
219 inline cic:/CoRN/reals/R_morphism/H2.var.
221 inline cic:/CoRN/reals/R_morphism/less_pres_f.con.
223 inline cic:/CoRN/reals/R_morphism/leEq_pres_f.con.
225 inline cic:/CoRN/reals/R_morphism/f_pres_leEq.con.
227 inline cic:/CoRN/reals/R_morphism/f_pres_apartness.con.
237 inline cic:/CoRN/reals/R_morphism/H3.var.
239 inline cic:/CoRN/reals/R_morphism/f_pres_Zero.con.
241 inline cic:/CoRN/reals/R_morphism/f_pres_minus.con.
243 inline cic:/CoRN/reals/R_morphism/f_pres_min.con.
250 Section with_plus_less.
253 inline cic:/CoRN/reals/R_morphism/H2.var.
255 inline cic:/CoRN/reals/R_morphism/H3.var.
257 inline cic:/CoRN/reals/R_morphism/f_pres_ap_zero.con.
260 Section surjectivity_helps.
263 inline cic:/CoRN/reals/R_morphism/f_surj.var.
265 inline cic:/CoRN/reals/R_morphism/f_pres_Lim.con.
268 End surjectivity_helps.
272 Section with_mult_plus_less.
275 inline cic:/CoRN/reals/R_morphism/H4.var.
277 inline cic:/CoRN/reals/R_morphism/f_pres_one.con.
279 inline cic:/CoRN/reals/R_morphism/f_pres_inv.con.
281 inline cic:/CoRN/reals/R_morphism/simplified_Homomorphism.con.
284 End with_mult_plus_less.