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
*)