X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FDifferentiability.ma;h=812a91e02c4001d8ade0f9a90559b3db229f3dcf;hb=0a9ed4329c069d2e06902934b6d1d58d3690959c;hp=ded63db55c4abf92f0c39d81a933a766238ebabf;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git diff --git a/matita/contribs/CoRN-Decl/ftc/Differentiability.ma b/matita/contribs/CoRN-Decl/ftc/Differentiability.ma index ded63db55..812a91e02 100644 --- a/matita/contribs/CoRN-Decl/ftc/Differentiability.ma +++ b/matita/contribs/CoRN-Decl/ftc/Differentiability.ma @@ -25,7 +25,7 @@ include "ftc/PartInterval.ma". include "ftc/DerivativeOps.ma". (* UNEXPORTED -Section Definitions. +Section Definitions *) (*#* *Differentiability @@ -61,7 +61,7 @@ problems. inline "cic:/CoRN/ftc/Differentiability/Diffble_I.con". (* UNEXPORTED -End Definitions. +End Definitions *) (* UNEXPORTED @@ -69,7 +69,7 @@ Implicit Arguments Diffble_I [a b]. *) (* UNEXPORTED -Section Local_Properties. +Section Local_Properties *) (*#* @@ -84,17 +84,17 @@ inline "cic:/CoRN/ftc/Differentiability/included_imp_diffble.con". A function differentiable in an interval is everywhere defined in that interval. *) -inline "cic:/CoRN/ftc/Differentiability/a.var". +alias id "a" = "cic:/CoRN/ftc/Differentiability/Local_Properties/a.var". -inline "cic:/CoRN/ftc/Differentiability/b.var". +alias id "b" = "cic:/CoRN/ftc/Differentiability/Local_Properties/b.var". -inline "cic:/CoRN/ftc/Differentiability/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab'.var". (* begin hide *) -inline "cic:/CoRN/ftc/Differentiability/Hab.con". +inline "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab.con" "Local_Properties__". -inline "cic:/CoRN/ftc/Differentiability/I.con". +inline "cic:/CoRN/ftc/Differentiability/Local_Properties/I.con" "Local_Properties__". (* end hide *) @@ -107,7 +107,7 @@ If a function has a derivative in an interval then it is differentiable in that inline "cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con". (* UNEXPORTED -End Local_Properties. +End Local_Properties *) (* UNEXPORTED @@ -115,29 +115,29 @@ Hint Resolve diffble_imp_inc: included. *) (* UNEXPORTED -Section Operations. +Section Operations *) (*#* All the algebraic results carry on. *) -inline "cic:/CoRN/ftc/Differentiability/a.var". +alias id "a" = "cic:/CoRN/ftc/Differentiability/Operations/a.var". -inline "cic:/CoRN/ftc/Differentiability/b.var". +alias id "b" = "cic:/CoRN/ftc/Differentiability/Operations/b.var". -inline "cic:/CoRN/ftc/Differentiability/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Operations/Hab'.var". (* begin hide *) -inline "cic:/CoRN/ftc/Differentiability/Hab.con". +inline "cic:/CoRN/ftc/Differentiability/Operations/Hab.con" "Operations__". -inline "cic:/CoRN/ftc/Differentiability/I.con". +inline "cic:/CoRN/ftc/Differentiability/Operations/I.con" "Operations__". (* end hide *) (* UNEXPORTED -Section Constants. +Section Constants *) inline "cic:/CoRN/ftc/Differentiability/Diffble_I_const.con". @@ -145,32 +145,32 @@ inline "cic:/CoRN/ftc/Differentiability/Diffble_I_const.con". inline "cic:/CoRN/ftc/Differentiability/Diffble_I_id.con". (* UNEXPORTED -End Constants. +End Constants *) (* UNEXPORTED -Section Well_Definedness. +Section Well_Definedness *) -inline "cic:/CoRN/ftc/Differentiability/F.var". +alias id "F" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/F.var". -inline "cic:/CoRN/ftc/Differentiability/H.var". +alias id "H" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/H.var". -inline "cic:/CoRN/ftc/Differentiability/diffF.var". +alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/diffF.var". inline "cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con". (* UNEXPORTED -End Well_Definedness. +End Well_Definedness *) -inline "cic:/CoRN/ftc/Differentiability/F.var". +alias id "F" = "cic:/CoRN/ftc/Differentiability/Operations/F.var". -inline "cic:/CoRN/ftc/Differentiability/G.var". +alias id "G" = "cic:/CoRN/ftc/Differentiability/Operations/G.var". -inline "cic:/CoRN/ftc/Differentiability/diffF.var". +alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Operations/diffF.var". -inline "cic:/CoRN/ftc/Differentiability/diffG.var". +alias id "diffG" = "cic:/CoRN/ftc/Differentiability/Operations/diffG.var". inline "cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con". @@ -180,41 +180,41 @@ inline "cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con". (* begin show *) -inline "cic:/CoRN/ftc/Differentiability/Gbnd.var". +alias id "Gbnd" = "cic:/CoRN/ftc/Differentiability/Operations/Gbnd.var". (* end show *) inline "cic:/CoRN/ftc/Differentiability/Diffble_I_recip.con". (* UNEXPORTED -End Operations. +End Operations *) (* UNEXPORTED -Section Corollaries. +Section Corollaries *) -inline "cic:/CoRN/ftc/Differentiability/a.var". +alias id "a" = "cic:/CoRN/ftc/Differentiability/Corollaries/a.var". -inline "cic:/CoRN/ftc/Differentiability/b.var". +alias id "b" = "cic:/CoRN/ftc/Differentiability/Corollaries/b.var". -inline "cic:/CoRN/ftc/Differentiability/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Corollaries/Hab'.var". (* begin hide *) -inline "cic:/CoRN/ftc/Differentiability/Hab.con". +inline "cic:/CoRN/ftc/Differentiability/Corollaries/Hab.con" "Corollaries__". -inline "cic:/CoRN/ftc/Differentiability/I.con". +inline "cic:/CoRN/ftc/Differentiability/Corollaries/I.con" "Corollaries__". (* end hide *) -inline "cic:/CoRN/ftc/Differentiability/F.var". +alias id "F" = "cic:/CoRN/ftc/Differentiability/Corollaries/F.var". -inline "cic:/CoRN/ftc/Differentiability/G.var". +alias id "G" = "cic:/CoRN/ftc/Differentiability/Corollaries/G.var". -inline "cic:/CoRN/ftc/Differentiability/diffF.var". +alias id "diffF" = "cic:/CoRN/ftc/Differentiability/Corollaries/diffF.var". -inline "cic:/CoRN/ftc/Differentiability/diffG.var". +alias id "diffG" = "cic:/CoRN/ftc/Differentiability/Corollaries/diffG.var". inline "cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con". @@ -222,16 +222,16 @@ inline "cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con". inline "cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con". -inline "cic:/CoRN/ftc/Differentiability/Gbnd.var". +alias id "Gbnd" = "cic:/CoRN/ftc/Differentiability/Corollaries/Gbnd.var". inline "cic:/CoRN/ftc/Differentiability/Diffble_I_div.con". (* UNEXPORTED -End Corollaries. +End Corollaries *) (* UNEXPORTED -Section Other_Properties. +Section Other_Properties *) (*#* @@ -239,11 +239,11 @@ Differentiability of families of functions is proved by induction using the constant and addition rules. *) -inline "cic:/CoRN/ftc/Differentiability/a.var". +alias id "a" = "cic:/CoRN/ftc/Differentiability/Other_Properties/a.var". -inline "cic:/CoRN/ftc/Differentiability/b.var". +alias id "b" = "cic:/CoRN/ftc/Differentiability/Other_Properties/b.var". -inline "cic:/CoRN/ftc/Differentiability/Hab'.var". +alias id "Hab'" = "cic:/CoRN/ftc/Differentiability/Other_Properties/Hab'.var". inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con". @@ -252,7 +252,7 @@ inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con". inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con". (* UNEXPORTED -End Other_Properties. +End Other_Properties *) (*#*