X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FContFunctions.ma;h=504a7d7a064111f114f4d29d9c6a365a65b15969;hb=HEAD;hp=b4fa706898f738223f65cab96de232d6827f79c1;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
index b4fa70689..504a7d7a0 100644
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
@@ -16,14 +16,14 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/metrics/ContFunctions".
 
+include "CoRN.ma".
+
 (* $Id: ContFunctions.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *)
 
-(* INCLUDE
-CPseudoMSpaces
-*)
+include "metrics/CPseudoMSpaces.ma".
 
 (* UNEXPORTED
-Section Continuous_functions.
+Section Continuous_functions
 *)
 
 (*#* **Continuous functions, uniformly continuous functions and Lipschitz functions
@@ -32,30 +32,30 @@ Let [A] and [B] be pseudo metric spaces.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/A.var.
+alias id "A" = "cic:/CoRN/metrics/ContFunctions/Continuous_functions/A.var".
 
-inline cic:/CoRN/metrics/ContFunctions/B.var.
+alias id "B" = "cic:/CoRN/metrics/ContFunctions/Continuous_functions/B.var".
 
 (*#*
 We will look at some notions of continuous functions.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/continuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/continuous'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous''.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous''.con".
 
-inline cic:/CoRN/metrics/ContFunctions/lipschitz.con.
+inline "cic:/CoRN/metrics/ContFunctions/lipschitz.con".
 
-inline cic:/CoRN/metrics/ContFunctions/lipschitz'.con.
+inline "cic:/CoRN/metrics/ContFunctions/lipschitz'.con".
 
 (* UNEXPORTED
-End Continuous_functions.
+End Continuous_functions
 *)
 
 (* UNEXPORTED
@@ -87,44 +87,44 @@ Implicit Arguments lipschitz' [A B].
 *)
 
 (* UNEXPORTED
-Section Lemmas.
+Section Lemmas
 *)
 
 (* begin hide *)
 
-inline cic:/CoRN/metrics/ContFunctions/nexp_power.con.
+inline "cic:/CoRN/metrics/ContFunctions/nexp_power.con".
 
 (* end hide *)
 
-inline cic:/CoRN/metrics/ContFunctions/continuous_imp_continuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/continuous_imp_continuous'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/continuous'_imp_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/continuous'_imp_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_uni_continuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_uni_continuous'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous''.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous''.con".
 
-inline cic:/CoRN/metrics/ContFunctions/lipschitz_imp_lipschitz'.con.
+inline "cic:/CoRN/metrics/ContFunctions/lipschitz_imp_lipschitz'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/lipschitz'_imp_lipschitz.con.
+inline "cic:/CoRN/metrics/ContFunctions/lipschitz'_imp_lipschitz.con".
 
 (*#*
 Every uniformly continuous function is continuous and 
 every Lipschitz function is uniformly continuous.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/lipschitz_imp_uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/lipschitz_imp_uni_continuous.con".
 
 (* UNEXPORTED
-End Lemmas.
+End Lemmas
 *)
 
 (* UNEXPORTED
-Section Identity.
+Section Identity
 *)
 
 (*#* **Identity 
@@ -135,18 +135,18 @@ The identity function is Lipschitz.
 Hence it is uniformly continuous and continuous.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/id_is_lipschitz.con.
+inline "cic:/CoRN/metrics/ContFunctions/id_is_lipschitz.con".
 
-inline cic:/CoRN/metrics/ContFunctions/id_is_uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/id_is_uni_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/id_is_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/id_is_continuous.con".
 
 (* UNEXPORTED
-End Identity.
+End Identity
 *)
 
 (* UNEXPORTED
-Section Constant.
+Section Constant
 *)
 
 (*#* **Constant functions
@@ -160,22 +160,22 @@ Any constant function is Lipschitz.
 Hence it is uniformly continuous and continuous.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/B.var.
+alias id "B" = "cic:/CoRN/metrics/ContFunctions/Constant/B.var".
 
-inline cic:/CoRN/metrics/ContFunctions/X.var.
+alias id "X" = "cic:/CoRN/metrics/ContFunctions/Constant/X.var".
 
-inline cic:/CoRN/metrics/ContFunctions/const_fun_is_lipschitz.con.
+inline "cic:/CoRN/metrics/ContFunctions/const_fun_is_lipschitz.con".
 
-inline cic:/CoRN/metrics/ContFunctions/const_fun_is_uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/const_fun_is_uni_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/const_fun_is_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/const_fun_is_continuous.con".
 
 (* UNEXPORTED
-End Constant.
+End Constant
 *)
 
 (* UNEXPORTED
-Section Composition.
+Section Composition
 *)
 
 (*#* **Composition
@@ -191,58 +191,58 @@ The composition of two Lipschitz/uniformly continous/continuous functions is
 again Lipschitz/uniformly continuous/continuous.
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/X.var.
+alias id "X" = "cic:/CoRN/metrics/ContFunctions/Composition/X.var".
 
-inline cic:/CoRN/metrics/ContFunctions/B.var.
+alias id "B" = "cic:/CoRN/metrics/ContFunctions/Composition/B.var".
 
-inline cic:/CoRN/metrics/ContFunctions/f.var.
+alias id "f" = "cic:/CoRN/metrics/ContFunctions/Composition/f.var".
 
-inline cic:/CoRN/metrics/ContFunctions/C.var.
+alias id "C" = "cic:/CoRN/metrics/ContFunctions/Composition/C.var".
 
-inline cic:/CoRN/metrics/ContFunctions/g.var.
+alias id "g" = "cic:/CoRN/metrics/ContFunctions/Composition/g.var".
 
-inline cic:/CoRN/metrics/ContFunctions/comp_resp_lipschitz.con.
+inline "cic:/CoRN/metrics/ContFunctions/comp_resp_lipschitz.con".
 
-inline cic:/CoRN/metrics/ContFunctions/comp_resp_uni_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/comp_resp_uni_continuous.con".
 
-inline cic:/CoRN/metrics/ContFunctions/comp_resp_continuous.con.
+inline "cic:/CoRN/metrics/ContFunctions/comp_resp_continuous.con".
 
 (* UNEXPORTED
-End Composition.
+End Composition
 *)
 
 (* UNEXPORTED
-Section Limit.
+Section Limit
 *)
 
 (*#* **Limit
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/MSseqLimit.con.
+inline "cic:/CoRN/metrics/ContFunctions/MSseqLimit.con".
 
 (* UNEXPORTED
 Implicit Arguments MSseqLimit [X].
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/MSseqLimit'.con.
+inline "cic:/CoRN/metrics/ContFunctions/MSseqLimit'.con".
 
 (* UNEXPORTED
 Implicit Arguments MSseqLimit' [X].
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/MSseqLimit_imp_MSseqLimit'.con.
+inline "cic:/CoRN/metrics/ContFunctions/MSseqLimit_imp_MSseqLimit'.con".
 
-inline cic:/CoRN/metrics/ContFunctions/MSseqLimit'_imp_MSseqLimit.con.
+inline "cic:/CoRN/metrics/ContFunctions/MSseqLimit'_imp_MSseqLimit.con".
 
-inline cic:/CoRN/metrics/ContFunctions/seqcontinuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/seqcontinuous'.con".
 
 (* UNEXPORTED
 Implicit Arguments seqcontinuous' [A B].
 *)
 
-inline cic:/CoRN/metrics/ContFunctions/continuous'_imp_seqcontinuous'.con.
+inline "cic:/CoRN/metrics/ContFunctions/continuous'_imp_seqcontinuous'.con".
 
 (* UNEXPORTED
-End Limit.
+End Limit
 *)