]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/contribs/CoRN-Decl/ftc/NthDerivative.ma
procedural: bug fixes
[helm.git] / matita / contribs / CoRN-Decl / ftc / NthDerivative.ma
index 7f918465b7027b92da291c86159047b602263c9d..180d8a7a2406c909671be36648e71de6e1ba70e0 100644 (file)
 
 set "baseuri" "cic:/matita/CoRN-Decl/ftc/NthDerivative".
 
+include "CoRN.ma".
+
 (* $Id: NthDerivative.v,v 1.5 2004/04/20 22:38:50 hinderer Exp $ *)
 
-(* INCLUDE
-Differentiability
-*)
+include "ftc/Differentiability.ma".
 
 (* UNEXPORTED
-Section Nth_Derivative.
+Section Nth_Derivative
 *)
 
 (*#* *Nth Derivative
@@ -42,21 +42,21 @@ We now study higher order differentiability.
 We first define what we mean by the derivative of order [n] of a function.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/a.var.
+alias id "a" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/a.var".
 
-inline cic:/CoRN/ftc/NthDerivative/b.var.
+alias id "b" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/b.var".
 
-inline cic:/CoRN/ftc/NthDerivative/Hab'.var.
+alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab'.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/NthDerivative/Hab.con.
+inline "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab.con" "Nth_Derivative__".
 
-inline cic:/CoRN/ftc/NthDerivative/I.con.
+inline "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/I.con" "Nth_Derivative__".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con.
+inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con".
 
 (*#*
 Unlike first order differentiability, for our definition to be
@@ -65,10 +65,10 @@ to be [n] times differentiable instead of quantifying over the
 [Derivative_I_n] relation.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con.
+inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con".
 
 (* UNEXPORTED
-End Nth_Derivative.
+End Nth_Derivative
 *)
 
 (* UNEXPORTED
@@ -80,7 +80,7 @@ Implicit Arguments Diffble_I_n [a b].
 *)
 
 (* UNEXPORTED
-Section Trivia.
+Section Trivia
 *)
 
 (*#* **Trivia
@@ -88,34 +88,34 @@ Section Trivia.
 These are the expected extensionality and uniqueness results.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/a.var.
+alias id "a" = "cic:/CoRN/ftc/NthDerivative/Trivia/a.var".
 
-inline cic:/CoRN/ftc/NthDerivative/b.var.
+alias id "b" = "cic:/CoRN/ftc/NthDerivative/Trivia/b.var".
 
-inline cic:/CoRN/ftc/NthDerivative/Hab'.var.
+alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Trivia/Hab'.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/NthDerivative/Hab.con.
+inline "cic:/CoRN/ftc/NthDerivative/Trivia/Hab.con" "Trivia__".
 
-inline cic:/CoRN/ftc/NthDerivative/I.con.
+inline "cic:/CoRN/ftc/NthDerivative/Trivia/I.con" "Trivia__".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con.
+inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con".
 
-inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con.
+inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con".
 
-inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con.
+inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con".
 
-inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con.
+inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con".
 
 (* UNEXPORTED
-End Trivia.
+End Trivia
 *)
 
 (* UNEXPORTED
-Section Basic_Results.
+Section Basic_Results
 *)
 
 (*#* **Basic Results
@@ -126,17 +126,17 @@ the relation of [n] times derivative, but focus rather on the
 definition of [Diffble_I_n].
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/a.var.
+alias id "a" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/a.var".
 
-inline cic:/CoRN/ftc/NthDerivative/b.var.
+alias id "b" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/b.var".
 
-inline cic:/CoRN/ftc/NthDerivative/Hab'.var.
+alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab'.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/NthDerivative/Hab.con.
+inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab.con" "Basic_Results__".
 
-inline cic:/CoRN/ftc/NthDerivative/I.con.
+inline "cic:/CoRN/ftc/NthDerivative/Basic_Results/I.con" "Basic_Results__".
 
 (* end hide *)
 
@@ -144,15 +144,15 @@ inline cic:/CoRN/ftc/NthDerivative/I.con.
 We begin by showing that having a higher order derivative implies being differentiable.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con.
+inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con".
 
-inline cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con.
+inline "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con".
 
 (*#*
 If a function is [n] times differentiable then it is also [m] times differentiable for every [m] less or equal than [n].
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con.
+inline "cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con".
 
 (*#*
 The next result consolidates our intuition that a function is [n]
@@ -160,34 +160,34 @@ times differentiable if we can build from it a chain of [n]
 derivatives.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con.
+inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con".
 
 (*#*
 As expected, an [n] times differentiable in [[a,b]] function must be
 defined in that interval.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con.
+inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con".
 
 (*#*
 Also, the notions of derivative and differentiability are related as expected.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con.
+inline "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con".
 
-inline cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con.
+inline "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con".
 
 (*#*
 From this we can prove that if [F] has an nth order derivative in
 [[a,b]] then both [F] and its derivative are defined in that interval.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con.
+inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con".
 
-inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con.
+inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con".
 
 (* UNEXPORTED
-Section aux.
+Section aux
 *)
 
 (*#*
@@ -196,55 +196,55 @@ First order differentiability is just a special case.
 
 (* begin show *)
 
-inline cic:/CoRN/ftc/NthDerivative/F.var.
+alias id "F" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/F.var".
 
-inline cic:/CoRN/ftc/NthDerivative/diffF.var.
+alias id "diffF" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffF.var".
 
-inline cic:/CoRN/ftc/NthDerivative/diffFn.var.
+alias id "diffFn" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffFn.var".
 
 (* end show *)
 
-inline cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con.
+inline "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con".
 
-inline cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con.
+inline "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con".
 
 (* UNEXPORTED
-End aux.
+End aux
 *)
 
 (*#*
 As usual, nth order derivability is preserved by shrinking the interval.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con.
+inline "cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con".
 
-inline cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con.
+inline "cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con".
 
 (*#*
 And finally we have an addition rule for the order of the derivative.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con.
+inline "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con".
 
 (* UNEXPORTED
-End Basic_Results.
+End Basic_Results
 *)
 
 (* UNEXPORTED
-Section More_Results.
+Section More_Results
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/a.var.
+alias id "a" = "cic:/CoRN/ftc/NthDerivative/More_Results/a.var".
 
-inline cic:/CoRN/ftc/NthDerivative/b.var.
+alias id "b" = "cic:/CoRN/ftc/NthDerivative/More_Results/b.var".
 
-inline cic:/CoRN/ftc/NthDerivative/Hab'.var.
+alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/More_Results/Hab'.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/NthDerivative/Hab.con.
+inline "cic:/CoRN/ftc/NthDerivative/More_Results/Hab.con" "More_Results__".
 
-inline cic:/CoRN/ftc/NthDerivative/I.con.
+inline "cic:/CoRN/ftc/NthDerivative/More_Results/I.con" "More_Results__".
 
 (* end hide *)
 
@@ -256,47 +256,47 @@ elimination which we would get if we had defined nth differentiability
 as an existential quantification of the nth derivative relation.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/n_deriv_I.con.
+inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I.con".
 
 (*#*
 This operator is well defined and works as expected.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con.
+inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con".
 
-inline cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con.
+inline "cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con".
 
-inline cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con.
+inline "cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con".
 
-inline cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con.
+inline "cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con".
 
 (*#*
 Some basic properties of this operation.
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con.
+inline "cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con".
 
-inline cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con.
+inline "cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con".
 
 (* UNEXPORTED
-End More_Results.
+End More_Results
 *)
 
 (* UNEXPORTED
-Section More_on_n_deriv.
+Section More_on_n_deriv
 *)
 
 (*#*
 Some not so basic properties of this operation (needed in rather specific situations).
 *)
 
-inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con.
+inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con".
 
-inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con.
+inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con".
 
-inline cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con.
+inline "cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con".
 
 (* UNEXPORTED
-End More_on_n_deriv.
+End More_on_n_deriv
 *)