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
%\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
*)
(* 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
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
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
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
*)