X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FComposition.ma;h=e5ae78e35d3ed9fa1c842e5a221f9212276ea101;hb=0a9ed4329c069d2e06902934b6d1d58d3690959c;hp=81debe75552c04dbf7bfb0678b39789afca5aa0e;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/ftc/Composition.ma b/matita/contribs/CoRN-Decl/ftc/Composition.ma index 81debe755..e5ae78e35 100644 --- a/matita/contribs/CoRN-Decl/ftc/Composition.ma +++ b/matita/contribs/CoRN-Decl/ftc/Composition.ma @@ -16,18 +16,18 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Composition". +include "CoRN.ma". + (* $Id: Composition.v,v 1.4 2004/04/23 10:00:58 lcf Exp $ *) -(* INCLUDE -MoreFunctions -*) +include "ftc/MoreFunctions.ma". (* UNEXPORTED -Section Maps_into_Compacts. +Section Maps_into_Compacts *) (* UNEXPORTED -Section Part_Funct. +Section Part_Funct *) (*#* *Composition @@ -53,60 +53,60 @@ mapped into another compact interval. We define this concept for partial functions, and prove some trivial results. *) -inline cic:/CoRN/ftc/Composition/F.var. +alias id "F" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/F.var". -inline cic:/CoRN/ftc/Composition/G.var. +alias id "G" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/G.var". -inline cic:/CoRN/ftc/Composition/a.var. +alias id "a" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/a.var". -inline cic:/CoRN/ftc/Composition/b.var. +alias id "b" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/b.var". -inline cic:/CoRN/ftc/Composition/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hab.var". -inline cic:/CoRN/ftc/Composition/c.var. +alias id "c" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/c.var". -inline cic:/CoRN/ftc/Composition/d.var. +alias id "d" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/d.var". -inline cic:/CoRN/ftc/Composition/Hcd.var. +alias id "Hcd" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hcd.var". (* begin hide *) -inline cic:/CoRN/ftc/Composition/I.con. +inline "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/I.con" "Maps_into_Compacts__Part_Funct__". (* end hide *) (* begin show *) -inline cic:/CoRN/ftc/Composition/Hf.var. +alias id "Hf" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/Hf.var". (* end show *) -inline cic:/CoRN/ftc/Composition/maps_into_compacts.con. +inline "cic:/CoRN/ftc/Composition/maps_into_compacts.con". (* begin show *) -inline cic:/CoRN/ftc/Composition/maps.var. +alias id "maps" = "cic:/CoRN/ftc/Composition/Maps_into_Compacts/Part_Funct/maps.var". (* end show *) -inline cic:/CoRN/ftc/Composition/maps_lemma'.con. +inline "cic:/CoRN/ftc/Composition/maps_lemma'.con". -inline cic:/CoRN/ftc/Composition/maps_lemma.con. +inline "cic:/CoRN/ftc/Composition/maps_lemma.con". -inline cic:/CoRN/ftc/Composition/maps_lemma_less.con. +inline "cic:/CoRN/ftc/Composition/maps_lemma_less.con". -inline cic:/CoRN/ftc/Composition/maps_lemma_inc.con. +inline "cic:/CoRN/ftc/Composition/maps_lemma_inc.con". (* UNEXPORTED -End Part_Funct. +End Part_Funct *) (* UNEXPORTED -End Maps_into_Compacts. +End Maps_into_Compacts *) (* UNEXPORTED -Section Mapping. +Section Mapping *) (*#* @@ -114,40 +114,40 @@ As was the case for division of partial functions, this condition completely characterizes the domain of the composite function. *) -inline cic:/CoRN/ftc/Composition/F.var. +alias id "F" = "cic:/CoRN/ftc/Composition/Mapping/F.var". -inline cic:/CoRN/ftc/Composition/G.var. +alias id "G" = "cic:/CoRN/ftc/Composition/Mapping/G.var". -inline cic:/CoRN/ftc/Composition/a.var. +alias id "a" = "cic:/CoRN/ftc/Composition/Mapping/a.var". -inline cic:/CoRN/ftc/Composition/b.var. +alias id "b" = "cic:/CoRN/ftc/Composition/Mapping/b.var". -inline cic:/CoRN/ftc/Composition/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/Composition/Mapping/Hab.var". -inline cic:/CoRN/ftc/Composition/c.var. +alias id "c" = "cic:/CoRN/ftc/Composition/Mapping/c.var". -inline cic:/CoRN/ftc/Composition/d.var. +alias id "d" = "cic:/CoRN/ftc/Composition/Mapping/d.var". -inline cic:/CoRN/ftc/Composition/Hcd.var. +alias id "Hcd" = "cic:/CoRN/ftc/Composition/Mapping/Hcd.var". (* begin show *) -inline cic:/CoRN/ftc/Composition/Hf.var. +alias id "Hf" = "cic:/CoRN/ftc/Composition/Mapping/Hf.var". -inline cic:/CoRN/ftc/Composition/Hg.var. +alias id "Hg" = "cic:/CoRN/ftc/Composition/Mapping/Hg.var". -inline cic:/CoRN/ftc/Composition/maps.var. +alias id "maps" = "cic:/CoRN/ftc/Composition/Mapping/maps.var". (* end show *) -inline cic:/CoRN/ftc/Composition/included_comp.con. +inline "cic:/CoRN/ftc/Composition/included_comp.con". (* UNEXPORTED -End Mapping. +End Mapping *) (* UNEXPORTED -Section Interval_Continuity. +Section Interval_Continuity *) (*#* **Continuity @@ -155,46 +155,46 @@ Section Interval_Continuity. We now prove that the composition of two continuous partial functions is continuous. *) -inline cic:/CoRN/ftc/Composition/a.var. +alias id "a" = "cic:/CoRN/ftc/Composition/Interval_Continuity/a.var". -inline cic:/CoRN/ftc/Composition/b.var. +alias id "b" = "cic:/CoRN/ftc/Composition/Interval_Continuity/b.var". -inline cic:/CoRN/ftc/Composition/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/Composition/I.con. +inline "cic:/CoRN/ftc/Composition/Interval_Continuity/I.con" "Interval_Continuity__". (* end hide *) -inline cic:/CoRN/ftc/Composition/c.var. +alias id "c" = "cic:/CoRN/ftc/Composition/Interval_Continuity/c.var". -inline cic:/CoRN/ftc/Composition/d.var. +alias id "d" = "cic:/CoRN/ftc/Composition/Interval_Continuity/d.var". -inline cic:/CoRN/ftc/Composition/Hcd.var. +alias id "Hcd" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hcd.var". -inline cic:/CoRN/ftc/Composition/F.var. +alias id "F" = "cic:/CoRN/ftc/Composition/Interval_Continuity/F.var". -inline cic:/CoRN/ftc/Composition/G.var. +alias id "G" = "cic:/CoRN/ftc/Composition/Interval_Continuity/G.var". (* begin show *) -inline cic:/CoRN/ftc/Composition/contF.var. +alias id "contF" = "cic:/CoRN/ftc/Composition/Interval_Continuity/contF.var". -inline cic:/CoRN/ftc/Composition/contG.var. +alias id "contG" = "cic:/CoRN/ftc/Composition/Interval_Continuity/contG.var". -inline cic:/CoRN/ftc/Composition/Hmap.var. +alias id "Hmap" = "cic:/CoRN/ftc/Composition/Interval_Continuity/Hmap.var". (* end show *) -inline cic:/CoRN/ftc/Composition/Continuous_I_comp.con. +inline "cic:/CoRN/ftc/Composition/Continuous_I_comp.con". (* UNEXPORTED -End Interval_Continuity. +End Interval_Continuity *) (* UNEXPORTED -Section Derivative. +Section Derivative *) (*#* **Derivative @@ -202,64 +202,64 @@ Section Derivative. We now work with the derivative relation and prove the chain rule for partial functions. *) -inline cic:/CoRN/ftc/Composition/F.var. +alias id "F" = "cic:/CoRN/ftc/Composition/Derivative/F.var". -inline cic:/CoRN/ftc/Composition/F'.var. +alias id "F'" = "cic:/CoRN/ftc/Composition/Derivative/F'.var". -inline cic:/CoRN/ftc/Composition/G.var. +alias id "G" = "cic:/CoRN/ftc/Composition/Derivative/G.var". -inline cic:/CoRN/ftc/Composition/G'.var. +alias id "G'" = "cic:/CoRN/ftc/Composition/Derivative/G'.var". -inline cic:/CoRN/ftc/Composition/a.var. +alias id "a" = "cic:/CoRN/ftc/Composition/Derivative/a.var". -inline cic:/CoRN/ftc/Composition/b.var. +alias id "b" = "cic:/CoRN/ftc/Composition/Derivative/b.var". -inline cic:/CoRN/ftc/Composition/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/Composition/Derivative/Hab'.var". -inline cic:/CoRN/ftc/Composition/c.var. +alias id "c" = "cic:/CoRN/ftc/Composition/Derivative/c.var". -inline cic:/CoRN/ftc/Composition/d.var. +alias id "d" = "cic:/CoRN/ftc/Composition/Derivative/d.var". -inline cic:/CoRN/ftc/Composition/Hcd'.var. +alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Derivative/Hcd'.var". (* begin hide *) -inline cic:/CoRN/ftc/Composition/Hab.con. +inline "cic:/CoRN/ftc/Composition/Derivative/Hab.con" "Derivative__". -inline cic:/CoRN/ftc/Composition/Hcd.con. +inline "cic:/CoRN/ftc/Composition/Derivative/Hcd.con" "Derivative__". -inline cic:/CoRN/ftc/Composition/I.con. +inline "cic:/CoRN/ftc/Composition/Derivative/I.con" "Derivative__". (* end hide *) (* begin show *) -inline cic:/CoRN/ftc/Composition/derF.var. +alias id "derF" = "cic:/CoRN/ftc/Composition/Derivative/derF.var". -inline cic:/CoRN/ftc/Composition/derG.var. +alias id "derG" = "cic:/CoRN/ftc/Composition/Derivative/derG.var". -inline cic:/CoRN/ftc/Composition/Hmap.var. +alias id "Hmap" = "cic:/CoRN/ftc/Composition/Derivative/Hmap.var". (* end show *) -inline cic:/CoRN/ftc/Composition/included_comp'.con. +inline "cic:/CoRN/ftc/Composition/included_comp'.con". -inline cic:/CoRN/ftc/Composition/maps'.con. +inline "cic:/CoRN/ftc/Composition/maps'.con". -inline cic:/CoRN/ftc/Composition/Derivative_I_comp.con. +inline "cic:/CoRN/ftc/Composition/Derivative_I_comp.con". (*#* The next lemma will be useful when we move on to differentiability. *) -inline cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con. +inline "cic:/CoRN/ftc/Composition/Diffble_I_comp_aux.con". (* UNEXPORTED -End Derivative. +End Derivative *) (* UNEXPORTED -Section Differentiability. +Section Differentiability *) (*#* **Differentiability @@ -267,50 +267,50 @@ Section Differentiability. Finally, we move on to differentiability. *) -inline cic:/CoRN/ftc/Composition/F.var. +alias id "F" = "cic:/CoRN/ftc/Composition/Differentiability/F.var". -inline cic:/CoRN/ftc/Composition/G.var. +alias id "G" = "cic:/CoRN/ftc/Composition/Differentiability/G.var". -inline cic:/CoRN/ftc/Composition/a.var. +alias id "a" = "cic:/CoRN/ftc/Composition/Differentiability/a.var". -inline cic:/CoRN/ftc/Composition/b.var. +alias id "b" = "cic:/CoRN/ftc/Composition/Differentiability/b.var". -inline cic:/CoRN/ftc/Composition/Hab'.var. +alias id "Hab'" = "cic:/CoRN/ftc/Composition/Differentiability/Hab'.var". -inline cic:/CoRN/ftc/Composition/c.var. +alias id "c" = "cic:/CoRN/ftc/Composition/Differentiability/c.var". -inline cic:/CoRN/ftc/Composition/d.var. +alias id "d" = "cic:/CoRN/ftc/Composition/Differentiability/d.var". -inline cic:/CoRN/ftc/Composition/Hcd'.var. +alias id "Hcd'" = "cic:/CoRN/ftc/Composition/Differentiability/Hcd'.var". (* begin hide *) -inline cic:/CoRN/ftc/Composition/Hab.con. +inline "cic:/CoRN/ftc/Composition/Differentiability/Hab.con" "Differentiability__". -inline cic:/CoRN/ftc/Composition/Hcd.con. +inline "cic:/CoRN/ftc/Composition/Differentiability/Hcd.con" "Differentiability__". -inline cic:/CoRN/ftc/Composition/I.con. +inline "cic:/CoRN/ftc/Composition/Differentiability/I.con" "Differentiability__". (* end hide *) (* begin show *) -inline cic:/CoRN/ftc/Composition/diffF.var. +alias id "diffF" = "cic:/CoRN/ftc/Composition/Differentiability/diffF.var". -inline cic:/CoRN/ftc/Composition/diffG.var. +alias id "diffG" = "cic:/CoRN/ftc/Composition/Differentiability/diffG.var". -inline cic:/CoRN/ftc/Composition/Hmap.var. +alias id "Hmap" = "cic:/CoRN/ftc/Composition/Differentiability/Hmap.var". (* end show *) -inline cic:/CoRN/ftc/Composition/Diffble_I_comp.con. +inline "cic:/CoRN/ftc/Composition/Diffble_I_comp.con". (* UNEXPORTED -End Differentiability. +End Differentiability *) (* UNEXPORTED -Section Generalized_Intervals. +Section Generalized_Intervals *) (*#* **Generalizations @@ -321,76 +321,76 @@ We now generalize this results to arbitrary intervals. We begin by generalizing %\end{convention}% *) -inline cic:/CoRN/ftc/Composition/I.var. +alias id "I" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/I.var". -inline cic:/CoRN/ftc/Composition/J.var. +alias id "J" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/J.var". -inline cic:/CoRN/ftc/Composition/pI.var. +alias id "pI" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pI.var". -inline cic:/CoRN/ftc/Composition/pJ.var. +alias id "pJ" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/pJ.var". -inline cic:/CoRN/ftc/Composition/maps_compacts_into.con. +inline "cic:/CoRN/ftc/Composition/maps_compacts_into.con". (*#* Now everything comes naturally: *) -inline cic:/CoRN/ftc/Composition/comp_inc_lemma.con. +inline "cic:/CoRN/ftc/Composition/comp_inc_lemma.con". -inline cic:/CoRN/ftc/Composition/F.var. +alias id "F" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F.var". -inline cic:/CoRN/ftc/Composition/F'.var. +alias id "F'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/F'.var". -inline cic:/CoRN/ftc/Composition/G.var. +alias id "G" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/G.var". -inline cic:/CoRN/ftc/Composition/G'.var. +alias id "G'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/G'.var". (* begin show *) -inline cic:/CoRN/ftc/Composition/Hmap.var. +alias id "Hmap" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap.var". (* end show *) -inline cic:/CoRN/ftc/Composition/Continuous_comp.con. +inline "cic:/CoRN/ftc/Composition/Continuous_comp.con". (* begin show *) -inline cic:/CoRN/ftc/Composition/Hmap'.var. +alias id "Hmap'" = "cic:/CoRN/ftc/Composition/Generalized_Intervals/Hmap'.var". (* end show *) -inline cic:/CoRN/ftc/Composition/Derivative_comp.con. +inline "cic:/CoRN/ftc/Composition/Derivative_comp.con". (* UNEXPORTED -End Generalized_Intervals. +End Generalized_Intervals *) (* UNEXPORTED -Section Corollaries. +Section Corollaries *) (*#* Finally, some criteria to prove that a function with a specific domain maps compacts into compacts: *) -inline cic:/CoRN/ftc/Composition/positive_fun.con. +inline "cic:/CoRN/ftc/Composition/positive_fun.con". -inline cic:/CoRN/ftc/Composition/negative_fun.con. +inline "cic:/CoRN/ftc/Composition/negative_fun.con". -inline cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con. +inline "cic:/CoRN/ftc/Composition/positive_imp_maps_compacts_into.con". -inline cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con. +inline "cic:/CoRN/ftc/Composition/negative_imp_maps_compacts_into.con". -inline cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con. +inline "cic:/CoRN/ftc/Composition/Continuous_imp_maps_compacts_into.con". (*#* As a corollary, we get the generalization of differentiability property. *) -inline cic:/CoRN/ftc/Composition/Diffble_comp.con. +inline "cic:/CoRN/ftc/Composition/Diffble_comp.con". (* UNEXPORTED -End Corollaries. +End Corollaries *) (* UNEXPORTED