...

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / ftc / Continuity.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/Continuity.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/Continuity.mma
index ff66216f52bbe1a5a5756e2a521d82fe27d8b6dd..f205054b98ef10867f0a1dd5e3c95361128bd93d 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/ftc/Continuity.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/Continuity.mma
@@ -52,11 +52,17 @@ respectively [P, Q] and [R].
 Here we define continuity and prove some basic properties of continuous functions.
 *)
 
-alias id "a" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/Hab.var
+*)
 
 (* begin hide *)
 
@@ -64,7 +70,9 @@ inline procedural "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/I.con"
 
 (* end hide *)
 
-alias id "F" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/F.var
+*)
 
 (* begin hide *)
 
@@ -86,7 +94,9 @@ inline procedural "cic:/CoRN/ftc/Continuity/contin_prop.con" as lemma.
 Assume [F] to be continuous in [I].  Then it has a least upper bound and a greater lower bound on [I].
 *)
 
-alias id "contF" = "cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Definitions_and_Basic_Results/contF.var
+*)
 
 (* begin hide *)
 
@@ -171,11 +181,17 @@ Section Local_Results
 We now state and prove some results about continuous functions.  Assume that [I] is included in the domain of both [F] and [G].
 *)
 
-alias id "a" = "cic:/CoRN/ftc/Continuity/Local_Results/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/Continuity/Local_Results/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/Continuity/Local_Results/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/Hab.var
+*)
 
 (* begin hide *)
 
@@ -183,9 +199,13 @@ inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/I.con" "Local_Results_
 
 (* end hide *)
 
-alias id "F" = "cic:/CoRN/ftc/Continuity/Local_Results/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/Continuity/Local_Results/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/G.var
+*)
 
 (* begin hide *)
 
@@ -195,9 +215,13 @@ inline procedural "cic:/CoRN/ftc/Continuity/Local_Results/Q.con" "Local_Results_
 
 (* end hide *)
 
-alias id "incF" = "cic:/CoRN/ftc/Continuity/Local_Results/incF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/incF.var
+*)
 
-alias id "incG" = "cic:/CoRN/ftc/Continuity/Local_Results/incG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/incG.var
+*)
 
 (*#*
 The first result does not require the function to be continuous; however, its preconditions are easily verified by continuous functions, which justifies its inclusion in this section.
@@ -233,9 +257,13 @@ inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_id.con" as lemma.
 Assume [F] and [G] are continuous in [I].  Then functions derived from these through algebraic operations are also continuous, provided (in the case of reciprocal and division) some extra conditions are met.
 *)
 
-alias id "contF" = "cic:/CoRN/ftc/Continuity/Local_Results/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/contF.var
+*)
 
-alias id "contG" = "cic:/CoRN/ftc/Continuity/Local_Results/contG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/contG.var
+*)
 
 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_plus.con" as lemma.
 
@@ -255,9 +283,13 @@ inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_max.con" as lemma.
 
 (* begin show *)
 
-alias id "Hg'" = "cic:/CoRN/ftc/Continuity/Local_Results/Hg'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/Hg'.var
+*)
 
-alias id "Hg''" = "cic:/CoRN/ftc/Continuity/Local_Results/Hg''.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Local_Results/Hg''.var
+*)
 
 (* end show *)
 
@@ -275,11 +307,17 @@ Hint Resolve contin_imp_inc: included.
 Section Corolaries
 *)
 
-alias id "a" = "cic:/CoRN/ftc/Continuity/Corolaries/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Corolaries/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/Continuity/Corolaries/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Corolaries/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/Continuity/Corolaries/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Corolaries/Hab.var
+*)
 
 (* begin hide *)
 
@@ -287,9 +325,13 @@ inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/I.con" "Corolaries__" as
 
 (* end hide *)
 
-alias id "F" = "cic:/CoRN/ftc/Continuity/Corolaries/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Corolaries/F.var
+*)
 
-alias id "G" = "cic:/CoRN/ftc/Continuity/Corolaries/G.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Corolaries/G.var
+*)
 
 (* begin hide *)
 
@@ -299,9 +341,13 @@ inline procedural "cic:/CoRN/ftc/Continuity/Corolaries/Q.con" "Corolaries__" as
 
 (* end hide *)
 
-alias id "contF" = "cic:/CoRN/ftc/Continuity/Corolaries/contF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Corolaries/contF.var
+*)
 
-alias id "contG" = "cic:/CoRN/ftc/Continuity/Corolaries/contG.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Corolaries/contG.var
+*)
 
 (*#*
 The corresponding properties for subtraction, division and
@@ -320,9 +366,13 @@ inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_min.con" as lemma.
 
 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_abs.con" as lemma.
 
-alias id "Hg'" = "cic:/CoRN/ftc/Continuity/Corolaries/Hg'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Corolaries/Hg'.var
+*)
 
-alias id "Hg''" = "cic:/CoRN/ftc/Continuity/Corolaries/Hg''.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Corolaries/Hg''.var
+*)
 
 inline procedural "cic:/CoRN/ftc/Continuity/Continuous_I_div.con" as lemma.
 
@@ -342,13 +392,21 @@ Section Sums
 We finally prove that the sum of an arbitrary family of continuous functions is still a continuous function.
 *)
 
-alias id "a" = "cic:/CoRN/ftc/Continuity/Other/Sums/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Other/Sums/a.var
+*)
 
-alias id "b" = "cic:/CoRN/ftc/Continuity/Other/Sums/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Other/Sums/b.var
+*)
 
-alias id "Hab" = "cic:/CoRN/ftc/Continuity/Other/Sums/Hab.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Other/Sums/Hab.var
+*)
 
-alias id "Hab'" = "cic:/CoRN/ftc/Continuity/Other/Sums/Hab'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/Continuity/Other/Sums/Hab'.var
+*)
 
 (* begin hide *)