set "baseuri" "cic:/matita/CoRN-Decl/metrics/Prod_Sub".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Prod_Sub.v,v 1.4 2004/04/23 10:01:02 lcf Exp $ *)
include "metrics/IR_CPMSpace.ma".
(* UNEXPORTED
-Section prodpsmetrics.
+Section prodpsmetrics
*)
(*#* **Product-Pseudo-Metric-Spaces
inline "cic:/CoRN/metrics/Prod_Sub/Prod0CPsMetricSpace.con".
(* UNEXPORTED
-End prodpsmetrics.
+End prodpsmetrics
*)
(* UNEXPORTED
-Section subpsmetrics.
+Section subpsmetrics
*)
(*#* **Sub-Pseudo-Metric-Spaces
inline "cic:/CoRN/metrics/Prod_Sub/dsub'_uni_continuous''.con".
(* UNEXPORTED
-End subpsmetrics.
+End subpsmetrics
*)