X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Freals%2FR_morphism.ma;h=5ce1b103c7284126a298148f76bfe0fe31dd8c42;hb=db235934efa41a0f38e79747f6db4f468367410b;hp=24e1a144d9fcadc6db70268d0180e72593d5fc91;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/R_morphism.ma b/helm/software/matita/contribs/CoRN-Decl/reals/R_morphism.ma index 24e1a144d..5ce1b103c 100644 --- a/helm/software/matita/contribs/CoRN-Decl/reals/R_morphism.ma +++ b/helm/software/matita/contribs/CoRN-Decl/reals/R_morphism.ma @@ -16,64 +16,66 @@ 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 -CReals -*) +include "reals/CReals.ma". (* This comes from CReals1.v *) -inline cic:/CoRN/reals/R_morphism/Cauchy_Lim_prop2.con. +inline "cic:/CoRN/reals/R_morphism/Cauchy_Lim_prop2.con". (* UNEXPORTED -Section morphism. +Section morphism *) -inline cic:/CoRN/reals/R_morphism/R1.var. +alias id "R1" = "cic:/CoRN/reals/R_morphism/morphism/R1.var". -inline cic:/CoRN/reals/R_morphism/R2.var. +alias id "R2" = "cic:/CoRN/reals/R_morphism/morphism/R2.var". (* UNEXPORTED -Section morphism_details. +Section morphism_details *) -inline cic:/CoRN/reals/R_morphism/phi.var. +alias id "phi" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/phi.var". -inline cic:/CoRN/reals/R_morphism/p1.var. +alias id "p1" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/p1.var". -inline cic:/CoRN/reals/R_morphism/p2.var. +alias id "p2" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/p2.var". -inline cic:/CoRN/reals/R_morphism/f1.var. +alias id "f1" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/f1.var". -inline cic:/CoRN/reals/R_morphism/f2.var. +alias id "f2" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/f2.var". -inline cic:/CoRN/reals/R_morphism/g1.var. +alias id "g1" = "cic:/CoRN/reals/R_morphism/morphism/morphism_details/g1.var". -inline cic:/CoRN/reals/R_morphism/g2.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_relation.con". -inline cic:/CoRN/reals/R_morphism/fun_pres_un_fun.con. +inline "cic:/CoRN/reals/R_morphism/fun_pres_un_fun.con". -inline cic:/CoRN/reals/R_morphism/fun_pres_bin_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. +inline "cic:/CoRN/reals/R_morphism/fun_pres_Lim.con". (* UNEXPORTED -End morphism_details. +End morphism_details *) -inline cic:/CoRN/reals/R_morphism/Homomorphism.ind. +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:= @@ -84,212 +86,212 @@ Definition Homo_as_CSetoid_fun:= ). *****************) -inline cic:/CoRN/reals/R_morphism/map_strext_unfolded.con. +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_wd_unfolded.con". -inline cic:/CoRN/reals/R_morphism/map_pres_less_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_plus_unfolded.con". -inline cic:/CoRN/reals/R_morphism/map_pres_mult_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.con". -inline cic:/CoRN/reals/R_morphism/map_pres_zero_unfolded.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.con". -inline cic:/CoRN/reals/R_morphism/map_pres_minus_unfolded.con. +inline "cic:/CoRN/reals/R_morphism/map_pres_minus_unfolded.con". -inline cic:/CoRN/reals/R_morphism/map_pres_apartness.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_ap_zero.con". -inline cic:/CoRN/reals/R_morphism/map_pres_one.con. +inline "cic:/CoRN/reals/R_morphism/map_pres_one.con". -inline cic:/CoRN/reals/R_morphism/map_pres_one_unfolded.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. +inline "cic:/CoRN/reals/R_morphism/map_pres_inv_unfolded.con". (* UNEXPORTED -End morphism. +End morphism *) (* UNEXPORTED -Section composition. +Section composition *) -inline cic:/CoRN/reals/R_morphism/R1.var. +alias id "R1" = "cic:/CoRN/reals/R_morphism/composition/R1.var". -inline cic:/CoRN/reals/R_morphism/R2.var. +alias id "R2" = "cic:/CoRN/reals/R_morphism/composition/R2.var". -inline cic:/CoRN/reals/R_morphism/R3.var. +alias id "R3" = "cic:/CoRN/reals/R_morphism/composition/R3.var". -inline cic:/CoRN/reals/R_morphism/f.var. +alias id "f" = "cic:/CoRN/reals/R_morphism/composition/f.var". -inline cic:/CoRN/reals/R_morphism/g.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.con". -inline cic:/CoRN/reals/R_morphism/compose_strext.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_less.con". -inline cic:/CoRN/reals/R_morphism/compose_pres_plus.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_mult.con". -inline cic:/CoRN/reals/R_morphism/compose_pres_Lim.con. +inline "cic:/CoRN/reals/R_morphism/compose_pres_Lim.con". -inline cic:/CoRN/reals/R_morphism/Compose.con. +inline "cic:/CoRN/reals/R_morphism/Compose.con". (* UNEXPORTED -End composition. +End composition *) (* UNEXPORTED -Section isomorphism. +Section isomorphism *) -inline cic:/CoRN/reals/R_morphism/R1.var. +alias id "R1" = "cic:/CoRN/reals/R_morphism/isomorphism/R1.var". -inline cic:/CoRN/reals/R_morphism/R2.var. +alias id "R2" = "cic:/CoRN/reals/R_morphism/isomorphism/R2.var". (* UNEXPORTED -Section identity_map. +Section identity_map *) -inline cic:/CoRN/reals/R_morphism/R3.var. +alias id "R3" = "cic:/CoRN/reals/R_morphism/isomorphism/identity_map/R3.var". -inline cic:/CoRN/reals/R_morphism/f.var. +alias id "f" = "cic:/CoRN/reals/R_morphism/isomorphism/identity_map/f.var". -inline cic:/CoRN/reals/R_morphism/map_is_id.con. +inline "cic:/CoRN/reals/R_morphism/map_is_id.con". (* UNEXPORTED -End identity_map. +End identity_map *) -inline cic:/CoRN/reals/R_morphism/Isomorphism.ind. +inline "cic:/CoRN/reals/R_morphism/Isomorphism.ind". (* UNEXPORTED -End isomorphism. +End isomorphism *) (* UNEXPORTED -Section surjective_map. +Section surjective_map *) -inline cic:/CoRN/reals/R_morphism/R1.var. +alias id "R1" = "cic:/CoRN/reals/R_morphism/surjective_map/R1.var". -inline cic:/CoRN/reals/R_morphism/R2.var. +alias id "R2" = "cic:/CoRN/reals/R_morphism/surjective_map/R2.var". -inline cic:/CoRN/reals/R_morphism/f.var. +alias id "f" = "cic:/CoRN/reals/R_morphism/surjective_map/f.var". -inline cic:/CoRN/reals/R_morphism/map_is_surjective.con. +inline "cic:/CoRN/reals/R_morphism/map_is_surjective.con". (* UNEXPORTED -End surjective_map. +End surjective_map *) (* UNEXPORTED -Section simplification. +Section simplification *) -inline cic:/CoRN/reals/R_morphism/R1.var. +alias id "R1" = "cic:/CoRN/reals/R_morphism/simplification/R1.var". -inline cic:/CoRN/reals/R_morphism/R2.var. +alias id "R2" = "cic:/CoRN/reals/R_morphism/simplification/R2.var". -inline cic:/CoRN/reals/R_morphism/f.var. +alias id "f" = "cic:/CoRN/reals/R_morphism/simplification/f.var". -inline cic:/CoRN/reals/R_morphism/H1.var. +alias id "H1" = "cic:/CoRN/reals/R_morphism/simplification/H1.var". -inline cic:/CoRN/reals/R_morphism/f_well_def.con. +inline "cic:/CoRN/reals/R_morphism/f_well_def.con". (* UNEXPORTED -Section with_less. +Section with_less *) -inline cic:/CoRN/reals/R_morphism/H2.var. +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/less_pres_f.con". -inline cic:/CoRN/reals/R_morphism/leEq_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_leEq.con". -inline cic:/CoRN/reals/R_morphism/f_pres_apartness.con. +inline "cic:/CoRN/reals/R_morphism/f_pres_apartness.con". (* UNEXPORTED -End with_less. +End with_less *) (* UNEXPORTED -Section with_plus. +Section with_plus *) -inline cic:/CoRN/reals/R_morphism/H3.var. +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_Zero.con". -inline cic:/CoRN/reals/R_morphism/f_pres_minus.con. +inline "cic:/CoRN/reals/R_morphism/f_pres_minus.con". -inline cic:/CoRN/reals/R_morphism/f_pres_min.con. +inline "cic:/CoRN/reals/R_morphism/f_pres_min.con". (* UNEXPORTED -End with_plus. +End with_plus *) (* UNEXPORTED -Section with_plus_less. +Section with_plus_less *) -inline cic:/CoRN/reals/R_morphism/H2.var. +alias id "H2" = "cic:/CoRN/reals/R_morphism/simplification/with_plus_less/H2.var". -inline cic:/CoRN/reals/R_morphism/H3.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. +inline "cic:/CoRN/reals/R_morphism/f_pres_ap_zero.con". (* UNEXPORTED -Section surjectivity_helps. +Section surjectivity_helps *) -inline cic:/CoRN/reals/R_morphism/f_surj.var. +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. +inline "cic:/CoRN/reals/R_morphism/f_pres_Lim.con". (* UNEXPORTED -End surjectivity_helps. +End surjectivity_helps *) (* UNEXPORTED -Section with_mult_plus_less. +Section with_mult_plus_less *) -inline cic:/CoRN/reals/R_morphism/H4.var. +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_one.con". -inline cic:/CoRN/reals/R_morphism/f_pres_inv.con. +inline "cic:/CoRN/reals/R_morphism/f_pres_inv.con". -inline cic:/CoRN/reals/R_morphism/simplified_Homomorphism.con. +inline "cic:/CoRN/reals/R_morphism/simplified_Homomorphism.con". (* UNEXPORTED -End with_mult_plus_less. +End with_mult_plus_less *) (* UNEXPORTED -End with_plus_less. +End with_plus_less *) (* UNEXPORTED -End simplification. +End simplification *) (* end hide *)