X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FDifferentiability.ma;h=aeb3bdcec3f35d89fa5dabd6debf0f937aec4f16;hb=5e01cba364607e7937aec2e359c34f049bb0f108;hp=898232c0e9dc32601a88126f4302951a99307fe9;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma index 898232c0e..aeb3bdcec 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma @@ -16,18 +16,16 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/Differentiability". +include "CoRN.ma". + (* $Id: Differentiability.v,v 1.5 2004/04/20 22:38:49 hinderer Exp $ *) -(* INCLUDE -PartInterval -*) +include "ftc/PartInterval.ma". -(* INCLUDE -DerivativeOps -*) +include "ftc/DerivativeOps.ma". (* UNEXPORTED -Section Definitions. +Section Definitions *) (*#* *Differentiability @@ -60,10 +58,10 @@ interval and eliminate the existencial quantifier without any problems. *) -inline cic:/CoRN/ftc/Differentiability/Diffble_I.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I.con". (* UNEXPORTED -End Definitions. +End Definitions *) (* UNEXPORTED @@ -71,7 +69,7 @@ Implicit Arguments Diffble_I [a b]. *) (* UNEXPORTED -Section Local_Properties. +Section Local_Properties *) (*#* @@ -80,36 +78,36 @@ From this point on, we just prove results analogous to the ones for derivability A function differentiable in [[a,b]] is differentiable in every proper compact subinterval of [[a,b]]. *) -inline cic:/CoRN/ftc/Differentiability/included_imp_diffble.con. +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. +inline "cic:/CoRN/ftc/Differentiability/Local_Properties/a.var" "Local_Properties__". -inline cic:/CoRN/ftc/Differentiability/b.var. +inline "cic:/CoRN/ftc/Differentiability/Local_Properties/b.var" "Local_Properties__". -inline cic:/CoRN/ftc/Differentiability/Hab'.var. +inline "cic:/CoRN/ftc/Differentiability/Local_Properties/Hab'.var" "Local_Properties__". (* 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 *) -inline cic:/CoRN/ftc/Differentiability/diffble_imp_inc.con. +inline "cic:/CoRN/ftc/Differentiability/diffble_imp_inc.con". (*#* If a function has a derivative in an interval then it is differentiable in that interval. *) -inline cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con. +inline "cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con". (* UNEXPORTED -End Local_Properties. +End Local_Properties *) (* UNEXPORTED @@ -117,123 +115,123 @@ Hint Resolve diffble_imp_inc: included. *) (* UNEXPORTED -Section Operations. +Section Operations *) (*#* All the algebraic results carry on. *) -inline cic:/CoRN/ftc/Differentiability/a.var. +inline "cic:/CoRN/ftc/Differentiability/Operations/a.var" "Operations__". -inline cic:/CoRN/ftc/Differentiability/b.var. +inline "cic:/CoRN/ftc/Differentiability/Operations/b.var" "Operations__". -inline cic:/CoRN/ftc/Differentiability/Hab'.var. +inline "cic:/CoRN/ftc/Differentiability/Operations/Hab'.var" "Operations__". (* 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. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_const.con". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_id.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. +inline "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/F.var" "Operations__Well_Definedness__". -inline cic:/CoRN/ftc/Differentiability/H.var. +inline "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/H.var" "Operations__Well_Definedness__". -inline cic:/CoRN/ftc/Differentiability/diffF.var. +inline "cic:/CoRN/ftc/Differentiability/Operations/Well_Definedness/diffF.var" "Operations__Well_Definedness__". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_wd.con". (* UNEXPORTED -End Well_Definedness. +End Well_Definedness *) -inline cic:/CoRN/ftc/Differentiability/F.var. +inline "cic:/CoRN/ftc/Differentiability/Operations/F.var" "Operations__". -inline cic:/CoRN/ftc/Differentiability/G.var. +inline "cic:/CoRN/ftc/Differentiability/Operations/G.var" "Operations__". -inline cic:/CoRN/ftc/Differentiability/diffF.var. +inline "cic:/CoRN/ftc/Differentiability/Operations/diffF.var" "Operations__". -inline cic:/CoRN/ftc/Differentiability/diffG.var. +inline "cic:/CoRN/ftc/Differentiability/Operations/diffG.var" "Operations__". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_plus.con". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_inv.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_inv.con". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_mult.con". (* begin show *) -inline cic:/CoRN/ftc/Differentiability/Gbnd.var. +inline "cic:/CoRN/ftc/Differentiability/Operations/Gbnd.var" "Operations__". (* end show *) -inline cic:/CoRN/ftc/Differentiability/Diffble_I_recip.con. +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. +inline "cic:/CoRN/ftc/Differentiability/Corollaries/a.var" "Corollaries__". -inline cic:/CoRN/ftc/Differentiability/b.var. +inline "cic:/CoRN/ftc/Differentiability/Corollaries/b.var" "Corollaries__". -inline cic:/CoRN/ftc/Differentiability/Hab'.var. +inline "cic:/CoRN/ftc/Differentiability/Corollaries/Hab'.var" "Corollaries__". (* 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. +inline "cic:/CoRN/ftc/Differentiability/Corollaries/F.var" "Corollaries__". -inline cic:/CoRN/ftc/Differentiability/G.var. +inline "cic:/CoRN/ftc/Differentiability/Corollaries/G.var" "Corollaries__". -inline cic:/CoRN/ftc/Differentiability/diffF.var. +inline "cic:/CoRN/ftc/Differentiability/Corollaries/diffF.var" "Corollaries__". -inline cic:/CoRN/ftc/Differentiability/diffG.var. +inline "cic:/CoRN/ftc/Differentiability/Corollaries/diffG.var" "Corollaries__". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_minus.con". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_scal.con". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_nth.con". -inline cic:/CoRN/ftc/Differentiability/Gbnd.var. +inline "cic:/CoRN/ftc/Differentiability/Corollaries/Gbnd.var" "Corollaries__". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_div.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_div.con". (* UNEXPORTED -End Corollaries. +End Corollaries *) (* UNEXPORTED -Section Other_Properties. +Section Other_Properties *) (*#* @@ -241,20 +239,20 @@ Differentiability of families of functions is proved by induction using the constant and addition rules. *) -inline cic:/CoRN/ftc/Differentiability/a.var. +inline "cic:/CoRN/ftc/Differentiability/Other_Properties/a.var" "Other_Properties__". -inline cic:/CoRN/ftc/Differentiability/b.var. +inline "cic:/CoRN/ftc/Differentiability/Other_Properties/b.var" "Other_Properties__". -inline cic:/CoRN/ftc/Differentiability/Hab'.var. +inline "cic:/CoRN/ftc/Differentiability/Other_Properties/Hab'.var" "Other_Properties__". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum0.con". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sumx.con". -inline cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con. +inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con". (* UNEXPORTED -End Other_Properties. +End Other_Properties *) (*#* @@ -264,7 +262,7 @@ Finally, a differentiable function is continuous. %\end{convention}% *) -inline cic:/CoRN/ftc/Differentiability/diffble_imp_contin_I.con. +inline "cic:/CoRN/ftc/Differentiability/diffble_imp_contin_I.con". (* UNEXPORTED Hint Immediate included_imp_contin deriv_imp_contin_I deriv_imp_contin'_I