set "baseuri" "cic:/matita/CoRN-Decl/ftc/Differentiability".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Differentiability.v,v 1.5 2004/04/20 22:38:49 hinderer Exp $ *)
include "ftc/DerivativeOps.ma".
(* UNEXPORTED
-Section Definitions.
+Section Definitions
*)
(*#* *Differentiability
inline "cic:/CoRN/ftc/Differentiability/Diffble_I.con".
(* UNEXPORTED
-End Definitions.
+End Definitions
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Local_Properties.
+Section Local_Properties
*)
(*#*
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 *)
inline "cic:/CoRN/ftc/Differentiability/deriv_imp_Diffble_I.con".
(* UNEXPORTED
-End Local_Properties.
+End Local_Properties
*)
(* UNEXPORTED
*)
(* 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".
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".
(* 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".
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
*)
(*#*
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".
inline "cic:/CoRN/ftc/Differentiability/Diffble_I_Sum.con".
(* UNEXPORTED
-End Other_Properties.
+End Other_Properties
*)
(*#*