set "baseuri" "cic:/matita/CoRN-Decl/metrics/CMetricSpaces".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CMetricSpaces.v,v 1.4 2004/04/23 10:01:01 lcf Exp $ *)
include "metrics/Equiv.ma".
(* UNEXPORTED
-Section Definition_MS.
+Section Definition_MS
*)
(*#* **Definition of Metric Space
inline "cic:/CoRN/metrics/CMetricSpaces/CMetricSpace.ind".
-coercion "cic:/matita/CoRN-Decl/metrics/CMetricSpaces/scms_crr.con" 0 (* compounds *).
+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
*)