X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FMoreFunctions.ma;h=4d7622ba2318fe4ae14baa440efc243b20854a5c;hb=HEAD;hp=8f0aeeda64233f21d1fa18b6ece10fd397ee6968;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma index 8f0aeeda6..4d7622ba2 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma @@ -16,20 +16,20 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreFunctions". +include "CoRN.ma". + (* $Id: MoreFunctions.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *) (*#* printing FNorm %\ensuremath{\|\cdot\|_{\infty}}% *) -(* INCLUDE -MoreIntervals -*) +include "ftc/MoreIntervals.ma". (* UNEXPORTED Opaque Min Max. *) (* UNEXPORTED -Section Basic_Results. +Section Basic_Results *) (*#* *More about Functions @@ -44,41 +44,41 @@ arbitrary intervals. **Continuity *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/I.var". (*#* Trivial stuff. *) -inline cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_imp_inc.con". (*#* %\begin{convention}% Assume that [I] is compact and [F] is continuous in [I]. %\end{convention}% *) -inline cic:/CoRN/ftc/MoreFunctions/cI.var. +alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/cI.var". -inline cic:/CoRN/ftc/MoreFunctions/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/F.var". -inline cic:/CoRN/ftc/MoreFunctions/contF.var. +alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/contF.var". -inline cic:/CoRN/ftc/MoreFunctions/continuous_compact.con. +inline "cic:/CoRN/ftc/MoreFunctions/continuous_compact.con". (* begin show *) -inline cic:/CoRN/ftc/MoreFunctions/Hinc.var. +alias id "Hinc" = "cic:/CoRN/ftc/MoreFunctions/Basic_Results/Hinc.var". (* end show *) -inline cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_I_imp_tb_image.con". -inline cic:/CoRN/ftc/MoreFunctions/FNorm.con. +inline "cic:/CoRN/ftc/MoreFunctions/FNorm.con". -inline cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con. +inline "cic:/CoRN/ftc/MoreFunctions/FNorm_bnd_AbsIR.con". (* UNEXPORTED -End Basic_Results. +End Basic_Results *) (* UNEXPORTED @@ -86,55 +86,55 @@ Hint Resolve Continuous_imp_inc: included. *) (* UNEXPORTED -Section Other_Results. +Section Other_Results *) (*#* The usual stuff. *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/I.var". -inline cic:/CoRN/ftc/MoreFunctions/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/F.var". -inline cic:/CoRN/ftc/MoreFunctions/G.var. +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/G.var". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_wd.con". (* begin show *) -inline cic:/CoRN/ftc/MoreFunctions/contF.var. +alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contF.var". -inline cic:/CoRN/ftc/MoreFunctions/contG.var. +alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Other_Results/contG.var". (* end show *) -inline cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con. +inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Continuous.con". -inline cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con. +inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Continuous.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_const.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_const.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_id.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_id.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_plus.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_inv.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_minus.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_mult.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_nth.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_scal.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_abs.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_recip.con". (* UNEXPORTED -End Other_Results. +End Other_Results *) (* UNEXPORTED @@ -148,27 +148,27 @@ Hint Immediate included_imp_Continuous Included_imp_Continuous: continuous. *) (* UNEXPORTED -Section Corollaries. +Section Corollaries *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/I.var". -inline cic:/CoRN/ftc/MoreFunctions/cI.var. +alias id "cI" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/cI.var". -inline cic:/CoRN/ftc/MoreFunctions/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/F.var". -inline cic:/CoRN/ftc/MoreFunctions/G.var. +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/G.var". -inline cic:/CoRN/ftc/MoreFunctions/contF.var. +alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contF.var". -inline cic:/CoRN/ftc/MoreFunctions/contG.var. +alias id "contG" = "cic:/CoRN/ftc/MoreFunctions/Corollaries/contG.var". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_div.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_div.con". -inline cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con. +inline "cic:/CoRN/ftc/MoreFunctions/FNorm_wd.con". (* UNEXPORTED -End Corollaries. +End Corollaries *) (* UNEXPORTED @@ -176,28 +176,28 @@ Hint Resolve Continuous_div: continuous. *) (* UNEXPORTED -Section Sums. +Section Sums *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Sums/I.var". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sumx.con". (*#* %\begin{convention}% Assume [f] is a sequence of continuous functions. %\end{convention}% *) -inline cic:/CoRN/ftc/MoreFunctions/f.var. +alias id "f" = "cic:/CoRN/ftc/MoreFunctions/Sums/f.var". -inline cic:/CoRN/ftc/MoreFunctions/contF.var. +alias id "contF" = "cic:/CoRN/ftc/MoreFunctions/Sums/contF.var". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum0.con". -inline cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con. +inline "cic:/CoRN/ftc/MoreFunctions/Continuous_Sum.con". (* UNEXPORTED -End Sums. +End Sums *) (* UNEXPORTED @@ -205,7 +205,7 @@ Hint Resolve Continuous_Sum0 Continuous_Sumx Continuous_Sum: continuous. *) (* UNEXPORTED -Section Basic_Properties. +Section Basic_Properties *) (*#* **Derivative @@ -216,32 +216,32 @@ Derivative is not that much different. %\end{convention}% *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/I.var". -inline cic:/CoRN/ftc/MoreFunctions/pI.var. +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/pI.var". -inline cic:/CoRN/ftc/MoreFunctions/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/F.var". -inline cic:/CoRN/ftc/MoreFunctions/G.var. +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/G.var". -inline cic:/CoRN/ftc/MoreFunctions/H.var. +alias id "H" = "cic:/CoRN/ftc/MoreFunctions/Basic_Properties/H.var". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdl.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_wdr.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_unique.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_inc'.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Continuous'.con". (* UNEXPORTED -End Basic_Properties. +End Basic_Properties *) (* UNEXPORTED @@ -254,118 +254,118 @@ Hint Immediate Derivative_imp_Continuous Derivative_imp_Continuous': *) (* UNEXPORTED -Section More_Results. +Section More_Results *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Results/I.var". -inline cic:/CoRN/ftc/MoreFunctions/pI.var. +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Results/pI.var". (*#* %\begin{convention}% Assume that [F'] and [G'] are derivatives of [F] and [G], respectively, in [I]. %\end{convention}% *) -inline cic:/CoRN/ftc/MoreFunctions/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F.var". -inline cic:/CoRN/ftc/MoreFunctions/F'.var. +alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/F'.var". -inline cic:/CoRN/ftc/MoreFunctions/G.var. +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G.var". -inline cic:/CoRN/ftc/MoreFunctions/G'.var. +alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Results/G'.var". -inline cic:/CoRN/ftc/MoreFunctions/derF.var. +alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derF.var". -inline cic:/CoRN/ftc/MoreFunctions/derG.var. +alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Results/derG.var". -inline cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con. +inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative.con". -inline cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con. +inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_const.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_const.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_id.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_id.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_plus.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_inv.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_minus.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_mult.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_scal.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_nth.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_recip.con". (* UNEXPORTED -End More_Results. +End More_Results *) (* UNEXPORTED -Section More_Corollaries. +Section More_Corollaries *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/I.var". -inline cic:/CoRN/ftc/MoreFunctions/pI.var. +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/pI.var". -inline cic:/CoRN/ftc/MoreFunctions/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F.var". -inline cic:/CoRN/ftc/MoreFunctions/F'.var. +alias id "F'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/F'.var". -inline cic:/CoRN/ftc/MoreFunctions/G.var. +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G.var". -inline cic:/CoRN/ftc/MoreFunctions/G'.var. +alias id "G'" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/G'.var". -inline cic:/CoRN/ftc/MoreFunctions/derF.var. +alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derF.var". -inline cic:/CoRN/ftc/MoreFunctions/derG.var. +alias id "derG" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/derG.var". (* begin show *) -inline cic:/CoRN/ftc/MoreFunctions/Gbnd.var. +alias id "Gbnd" = "cic:/CoRN/ftc/MoreFunctions/More_Corollaries/Gbnd.var". (* end show *) -inline cic:/CoRN/ftc/MoreFunctions/Derivative_div.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_div.con". (* UNEXPORTED -End More_Corollaries. +End More_Corollaries *) (* UNEXPORTED -Section More_Sums. +Section More_Sums *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/I.var". -inline cic:/CoRN/ftc/MoreFunctions/pI.var. +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/pI.var". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sumx.con". (* begin show *) -inline cic:/CoRN/ftc/MoreFunctions/f.var. +alias id "f" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f.var". -inline cic:/CoRN/ftc/MoreFunctions/f'.var. +alias id "f'" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/f'.var". -inline cic:/CoRN/ftc/MoreFunctions/derF.var. +alias id "derF" = "cic:/CoRN/ftc/MoreFunctions/More_Sums/derF.var". (* end show *) -inline cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum0.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_Sum.con". (* UNEXPORTED -End More_Sums. +End More_Sums *) (* UNEXPORTED -Section Diffble_Basic_Properties. +Section Diffble_Basic_Properties *) (*#* **Differentiability @@ -373,53 +373,53 @@ Section Diffble_Basic_Properties. Mutatis mutandis for differentiability. *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/I.var". -inline cic:/CoRN/ftc/MoreFunctions/pI.var. +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/pI.var". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_inc.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_imp_Diffble.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_wd.con". -inline cic:/CoRN/ftc/MoreFunctions/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/F.var". -inline cic:/CoRN/ftc/MoreFunctions/G.var. +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/G.var". -inline cic:/CoRN/ftc/MoreFunctions/diffF.var. +alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffF.var". -inline cic:/CoRN/ftc/MoreFunctions/diffG.var. +alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Basic_Properties/diffG.var". (*#* %\begin{convention}% Assume [F] and [G] are differentiable in [I]. %\end{convention}% *) -inline cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con. +inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble.con". -inline cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con. +inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_const.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_const.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_id.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_id.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_plus.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_inv.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_minus.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_mult.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_nth.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_scal.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_recip.con". (* UNEXPORTED -End Diffble_Basic_Properties. +End Diffble_Basic_Properties *) (* UNEXPORTED @@ -427,35 +427,35 @@ Hint Immediate Diffble_imp_inc: included. *) (* UNEXPORTED -Section Diffble_Corollaries. +Section Diffble_Corollaries *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/I.var". -inline cic:/CoRN/ftc/MoreFunctions/pI.var. +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/pI.var". -inline cic:/CoRN/ftc/MoreFunctions/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/F.var". -inline cic:/CoRN/ftc/MoreFunctions/G.var. +alias id "G" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/G.var". -inline cic:/CoRN/ftc/MoreFunctions/diffF.var. +alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffF.var". -inline cic:/CoRN/ftc/MoreFunctions/diffG.var. +alias id "diffG" = "cic:/CoRN/ftc/MoreFunctions/Diffble_Corollaries/diffG.var". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_div.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_div.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum0.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sumx.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_Sum.con". (* UNEXPORTED -End Diffble_Corollaries. +End Diffble_Corollaries *) (* UNEXPORTED -Section Nth_Derivative. +Section Nth_Derivative *) (*#* **Nth Derivative @@ -463,12 +463,12 @@ Section Nth_Derivative. Higher order derivatives pose more interesting problems. It turns out that it really becomes necessary to generalize our [n_deriv] operator to any interval. *) -inline cic:/CoRN/ftc/MoreFunctions/I.var. +alias id "I" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/I.var". -inline cic:/CoRN/ftc/MoreFunctions/pI.var. +alias id "pI" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/pI.var". (* UNEXPORTED -Section Definitions. +Section Definitions *) (*#* @@ -476,155 +476,155 @@ Section Definitions. %\end{convention}% *) -inline cic:/CoRN/ftc/MoreFunctions/n.var. +alias id "n" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/n.var". -inline cic:/CoRN/ftc/MoreFunctions/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/F.var". -inline cic:/CoRN/ftc/MoreFunctions/diffF.var. +alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Definitions/diffF.var". -inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con. +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_fun.con". -inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_char - (* begin hide *).con. +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_char + (* begin hide *).con". (* end hide *) -inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con. +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_strext.con". -inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con. +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_wd.con". -inline cic:/CoRN/ftc/MoreFunctions/N_Deriv.con. +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv.con". (* UNEXPORTED -End Definitions. +End Definitions *) (* UNEXPORTED -Section Basic_Results. +Section Basic_Results *) (*#* All the usual results hold. *) -inline cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_wd.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdr.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_wdl.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_unique.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_Diffble.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble.con". -inline cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con. +inline "cic:/CoRN/ftc/MoreFunctions/le_imp_Diffble_n.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_le.con". -inline cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_n_imp_inc.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Diffble_n.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_inc'.con". -inline cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con. +inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Derivative_n.con". -inline cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con. +inline "cic:/CoRN/ftc/MoreFunctions/included_imp_Diffble_n.con". -inline cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con. +inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Derivative_n.con". -inline cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con. +inline "cic:/CoRN/ftc/MoreFunctions/Included_imp_Diffble_n.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_plus.con". (* UNEXPORTED -End Basic_Results. +End Basic_Results *) (* UNEXPORTED -Section More_Results. +Section More_Results *) (*#* Some new results hold, too: *) -inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con. +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_Feq.con". -inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con. +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_lemma.con". -inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con. +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_S.con". -inline cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con. +inline "cic:/CoRN/ftc/MoreFunctions/N_Deriv_plus.con". (*#* Some useful characterization results. *) -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_O.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_Sn.con". (* UNEXPORTED -End More_Results. +End More_Results *) (* UNEXPORTED -Section Derivating_Diffble. +Section Derivating_Diffble *) (*#* As a special case we get a differentiation operator%\ldots%#...# *) -inline cic:/CoRN/ftc/MoreFunctions/F.var. +alias id "F" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/F.var". (* begin show *) -inline cic:/CoRN/ftc/MoreFunctions/diffF.var. +alias id "diffF" = "cic:/CoRN/ftc/MoreFunctions/Nth_Derivative/Derivating_Diffble/diffF.var". (* end show *) -inline cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con. +inline "cic:/CoRN/ftc/MoreFunctions/Diffble_imp_Diffble_n.con". -inline cic:/CoRN/ftc/MoreFunctions/Deriv.con. +inline "cic:/CoRN/ftc/MoreFunctions/Deriv.con". (* UNEXPORTED -End Derivating_Diffble. +End Derivating_Diffble *) (* UNEXPORTED -Section Corollaries. +Section Corollaries *) (*#* %\ldots%#...# for which the expected property also holds. *) -inline cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con. +inline "cic:/CoRN/ftc/MoreFunctions/Deriv_lemma.con". (*#* Some more interesting properties. *) -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_1.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_chain.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous.con". -inline cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con. +inline "cic:/CoRN/ftc/MoreFunctions/Derivative_n_imp_Continuous'.con". (* UNEXPORTED -End Corollaries. +End Corollaries *) (* UNEXPORTED -End Nth_Derivative. +End Nth_Derivative *) (* UNEXPORTED