include "metrics/Equiv.ma".
(* UNEXPORTED
-Section Definition_MS.
+Section Definition_MS
*)
(*#* **Definition of Metric Space
coercion cic:/matita/CoRN-Decl/metrics/CMetricSpaces/scms_crr.con 0 (* compounds *).
(* UNEXPORTED
-End Definition_MS.
+End Definition_MS
*)
(* UNEXPORTED
-Section MS_basics.
+Section MS_basics
*)
(*#* **Metric Space basics
inline "cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con".
(* UNEXPORTED
-End MS_basics.
+End MS_basics
*)
(* UNEXPORTED
-Section prodandsub.
+Section prodandsub
*)
(*#* **Product-Metric-Spaces and Sub-Metric-Spaces
*)
(* UNEXPORTED
-End prodandsub.
+End prodandsub
*)
(* UNEXPORTED
-Section Zeroff.
+Section Zeroff
*)
(*#* **Pseudo Metric Spaces vs Metric Spaces
inline "cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con".
(* UNEXPORTED
-End Zeroff.
+End Zeroff
*)
(* UNEXPORTED
-Section Limitt.
+Section Limitt
*)
(*#* **Limit
inline "cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con".
(* UNEXPORTED
-End Limitt.
+End Limitt
*)