X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Freals%2FR_morphism.ma;fp=matita%2Fcontribs%2FCoRN-Decl%2Freals%2FR_morphism.ma;h=5ce1b103c7284126a298148f76bfe0fe31dd8c42;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/CoRN-Decl/reals/R_morphism.ma b/matita/contribs/CoRN-Decl/reals/R_morphism.ma new file mode 100644 index 000000000..5ce1b103c --- /dev/null +++ b/matita/contribs/CoRN-Decl/reals/R_morphism.ma @@ -0,0 +1,298 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/CoRN-Decl/reals/R_morphism". + +include "CoRN.ma". + +(* begin hide *) + +(* In this file a notion of morphism between two arbitrary real number + structures, is introduced together with te proofs that this notion of + morphism preserves the basic algebraic structure. *) + +include "reals/CReals.ma". + +(* This comes from CReals1.v *) + +inline "cic:/CoRN/reals/R_morphism/Cauchy_Lim_prop2.con". + +(* UNEXPORTED +Section morphism +*) + +alias id "R1" = "cic:/CoRN/reals/R_morphism/morphism/R1.var". + +alias id "R2" = "cic:/CoRN/reals/R_morphism/morphism/R2.var". + +(* UNEXPORTED +Section morphism_details +*) + +alias id "phi" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/phi.var". + +alias id "p1" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/p1.var". + +alias id "p2" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/p2.var". + +alias id "f1" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/f1.var". + +alias id "f2" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/f2.var". + +alias id "g1" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/g1.var". + +alias id "g2" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/g2.var". + +inline "cic:/CoRN/reals/R_morphism/fun_pres_relation.con". + +inline "cic:/CoRN/reals/R_morphism/fun_pres_un_fun.con". + +inline "cic:/CoRN/reals/R_morphism/fun_pres_bin_fun.con". + +(* +Definition fun_pres_partial_fun:=(x:R1;H1:x[#]Zero;H2:(phi x)[#]Zero) +(phi (nzinj R1 (i1 (nzpro R1 x H1))))[=](nzinj R2 (i2 (nzpro R2 (phi x) H2))). +*) + +inline "cic:/CoRN/reals/R_morphism/fun_pres_Lim.con". + +(* UNEXPORTED +End morphism_details +*) + +inline "cic:/CoRN/reals/R_morphism/Homomorphism.ind". + +coercion cic:/matita/CoRN-Decl/reals/R_morphism/map.con 0 (* compounds *). + +(* This might be useful later... +Definition Homo_as_CSetoid_fun:= + [f:Homomorphism] + (Build_CSetoid_fun R1 R2 f + (fun_strext_imp_wd R1 R2 f (!map_strext f)) + (!map_strext f) + ). +*****************) + +inline "cic:/CoRN/reals/R_morphism/map_strext_unfolded.con". + +inline "cic:/CoRN/reals/R_morphism/map_wd_unfolded.con". + +inline "cic:/CoRN/reals/R_morphism/map_pres_less_unfolded.con". + +inline "cic:/CoRN/reals/R_morphism/map_pres_plus_unfolded.con". + +inline "cic:/CoRN/reals/R_morphism/map_pres_mult_unfolded.con". + +(* Now we start to derive some useful properties of a Homomorphism *) + +inline "cic:/CoRN/reals/R_morphism/map_pres_zero.con". + +inline "cic:/CoRN/reals/R_morphism/map_pres_zero_unfolded.con". + +inline "cic:/CoRN/reals/R_morphism/map_pres_minus.con". + +inline "cic:/CoRN/reals/R_morphism/map_pres_minus_unfolded.con". + +inline "cic:/CoRN/reals/R_morphism/map_pres_apartness.con". + +(* Merely a useful special case *) + +inline "cic:/CoRN/reals/R_morphism/map_pres_ap_zero.con". + +inline "cic:/CoRN/reals/R_morphism/map_pres_one.con". + +inline "cic:/CoRN/reals/R_morphism/map_pres_one_unfolded.con". + +(* I will not use the following lemma *) + +inline "cic:/CoRN/reals/R_morphism/map_pres_inv_unfolded.con". + +(* UNEXPORTED +End morphism +*) + +(* UNEXPORTED +Section composition +*) + +alias id "R1" = "cic:/CoRN/reals/R_morphism/composition/R1.var". + +alias id "R2" = "cic:/CoRN/reals/R_morphism/composition/R2.var". + +alias id "R3" = "cic:/CoRN/reals/R_morphism/composition/R3.var". + +alias id "f" = "cic:/CoRN/reals/R_morphism/composition/f.var". + +alias id "g" = "cic:/CoRN/reals/R_morphism/composition/g.var". + +inline "cic:/CoRN/reals/R_morphism/compose.con". + +inline "cic:/CoRN/reals/R_morphism/compose_strext.con". + +inline "cic:/CoRN/reals/R_morphism/compose_pres_less.con". + +inline "cic:/CoRN/reals/R_morphism/compose_pres_plus.con". + +inline "cic:/CoRN/reals/R_morphism/compose_pres_mult.con". + +inline "cic:/CoRN/reals/R_morphism/compose_pres_Lim.con". + +inline "cic:/CoRN/reals/R_morphism/Compose.con". + +(* UNEXPORTED +End composition +*) + +(* UNEXPORTED +Section isomorphism +*) + +alias id "R1" = "cic:/CoRN/reals/R_morphism/isomorphism/R1.var". + +alias id "R2" = "cic:/CoRN/reals/R_morphism/isomorphism/R2.var". + +(* UNEXPORTED +Section identity_map +*) + +alias id "R3" = "cic:/CoRN/reals/R_morphism/isomorphism/identity_map/R3.var". + +alias id "f" = "cic:/CoRN/reals/R_morphism/isomorphism/identity_map/f.var". + +inline "cic:/CoRN/reals/R_morphism/map_is_id.con". + +(* UNEXPORTED +End identity_map +*) + +inline "cic:/CoRN/reals/R_morphism/Isomorphism.ind". + +(* UNEXPORTED +End isomorphism +*) + +(* UNEXPORTED +Section surjective_map +*) + +alias id "R1" = "cic:/CoRN/reals/R_morphism/surjective_map/R1.var". + +alias id "R2" = "cic:/CoRN/reals/R_morphism/surjective_map/R2.var". + +alias id "f" = "cic:/CoRN/reals/R_morphism/surjective_map/f.var". + +inline "cic:/CoRN/reals/R_morphism/map_is_surjective.con". + +(* UNEXPORTED +End surjective_map +*) + +(* UNEXPORTED +Section simplification +*) + +alias id "R1" = "cic:/CoRN/reals/R_morphism/simplification/R1.var". + +alias id "R2" = "cic:/CoRN/reals/R_morphism/simplification/R2.var". + +alias id "f" = "cic:/CoRN/reals/R_morphism/simplification/f.var". + +alias id "H1" = "cic:/CoRN/reals/R_morphism/simplification/H1.var". + +inline "cic:/CoRN/reals/R_morphism/f_well_def.con". + +(* UNEXPORTED +Section with_less +*) + +alias id "H2" = "cic:/CoRN/reals/R_morphism/simplification/with_less/H2.var". + +inline "cic:/CoRN/reals/R_morphism/less_pres_f.con". + +inline "cic:/CoRN/reals/R_morphism/leEq_pres_f.con". + +inline "cic:/CoRN/reals/R_morphism/f_pres_leEq.con". + +inline "cic:/CoRN/reals/R_morphism/f_pres_apartness.con". + +(* UNEXPORTED +End with_less +*) + +(* UNEXPORTED +Section with_plus +*) + +alias id "H3" = "cic:/CoRN/reals/R_morphism/simplification/with_plus/H3.var". + +inline "cic:/CoRN/reals/R_morphism/f_pres_Zero.con". + +inline "cic:/CoRN/reals/R_morphism/f_pres_minus.con". + +inline "cic:/CoRN/reals/R_morphism/f_pres_min.con". + +(* UNEXPORTED +End with_plus +*) + +(* UNEXPORTED +Section with_plus_less +*) + +alias id "H2" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H2.var". + +alias id "H3" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H3.var". + +inline "cic:/CoRN/reals/R_morphism/f_pres_ap_zero.con". + +(* UNEXPORTED +Section surjectivity_helps +*) + +alias id "f_surj" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/surjectivity_helps/f_surj.var". + +inline "cic:/CoRN/reals/R_morphism/f_pres_Lim.con". + +(* UNEXPORTED +End surjectivity_helps +*) + +(* UNEXPORTED +Section with_mult_plus_less +*) + +alias id "H4" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/with_mult_plus_less/H4.var". + +inline "cic:/CoRN/reals/R_morphism/f_pres_one.con". + +inline "cic:/CoRN/reals/R_morphism/f_pres_inv.con". + +inline "cic:/CoRN/reals/R_morphism/simplified_Homomorphism.con". + +(* UNEXPORTED +End with_mult_plus_less +*) + +(* UNEXPORTED +End with_plus_less +*) + +(* UNEXPORTED +End simplification +*) + +(* end hide *) +