set "baseuri" "cic:/matita/CoRN-Decl/metrics/CMetricSpaces".
+include "CoRN.ma".
+
(* $Id: CMetricSpaces.v,v 1.4 2004/04/23 10:01:01 lcf Exp $ *)
-(* INCLUDE
-Prod_Sub
-*)
+include "metrics/Prod_Sub.ma".
-(* INCLUDE
-Equiv
-*)
+include "metrics/Equiv.ma".
(* UNEXPORTED
-Section Definition_MS.
+Section Definition_MS
*)
(*#* **Definition of Metric Space
*)
-inline cic:/CoRN/metrics/CMetricSpaces/CMetricSpace.ind.
+inline "cic:/CoRN/metrics/CMetricSpaces/CMetricSpace.ind".
+
+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/d_CMetricSpace_apdiag_imp_grzero.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/d_CMetricSpace_apdiag_imp_grzero.con".
-inline cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con".
-inline cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con.
+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
The product of two metric spaces is again a metric space.
*)
-inline cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpaces_apdiag_grzero.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpaces_apdiag_grzero.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpace.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpace.con".
(*#*
A subspace of a metric space is again a metric space.
Implicit Arguments SubPsMetricSpace [X].
*)
-inline cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace_apdiag_grzero.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace_apdiag_grzero.con".
-inline cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace.con".
(* UNEXPORTED
Implicit Arguments SubMetricSpace [X].
*)
(* UNEXPORTED
-End prodandsub.
+End prodandsub
*)
(* UNEXPORTED
-Section Zeroff.
+Section Zeroff
*)
(*#* **Pseudo Metric Spaces vs Metric Spaces
Not all pseudo metric spaces are a metric space:
*)
-inline cic:/CoRN/metrics/CMetricSpaces/zf_nis_CMetricSpace.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/zf_nis_CMetricSpace.con".
(*#*
But a pseudo metric space induces a metric space:
*)
-inline cic:/CoRN/metrics/CMetricSpaces/metric_ap.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/metric_ap.con".
-inline cic:/CoRN/metrics/CMetricSpaces/metric_eq.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/metric_eq.con".
-inline cic:/CoRN/metrics/CMetricSpaces/metric_ap_irreflexive.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/metric_ap_irreflexive.con".
-inline cic:/CoRN/metrics/CMetricSpaces/metric_ap_symmetric.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/metric_ap_symmetric.con".
-inline cic:/CoRN/metrics/CMetricSpaces/metric_ap_cotransitive.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/metric_ap_cotransitive.con".
-inline cic:/CoRN/metrics/CMetricSpaces/metric_ap_tight.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/metric_ap_tight.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Metric_CSet_is_CSetoid.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Metric_CSet_is_CSetoid.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Metric_CSetoid.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Metric_CSetoid.con".
-inline cic:/CoRN/metrics/CMetricSpaces/metric_d.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/metric_d.con".
-inline cic:/CoRN/metrics/CMetricSpaces/metric_d_strext.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/metric_d_strext.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Metric_d.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Metric_d_com.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d_com.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Metric_d_nneg.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d_nneg.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Metric_d_pos_imp_ap.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d_pos_imp_ap.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Metric_d_tri_ineq.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d_tri_ineq.con".
-inline cic:/CoRN/metrics/CMetricSpaces/QuotientCSetoid_is_CPsMetricSpace.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/QuotientCSetoid_is_CPsMetricSpace.con".
-inline cic:/CoRN/metrics/CMetricSpaces/QuotientCPsMetricSpace.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/QuotientCPsMetricSpace.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Metric_d_apdiag_grzero.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d_apdiag_grzero.con".
-inline cic:/CoRN/metrics/CMetricSpaces/QuotientCMetricSpace.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/QuotientCMetricSpace.con".
(*#*
Some pseudo metric spaces already are a metric space:
*)
-inline cic:/CoRN/metrics/CMetricSpaces/dIR_apdiag_grzero.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/dIR_apdiag_grzero.con".
-inline cic:/CoRN/metrics/CMetricSpaces/IR_as_CMetricSpace.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/IR_as_CMetricSpace.con".
(*#*
In that case the induced metric space is equivalent to the original one:
*)
-inline cic:/CoRN/metrics/CMetricSpaces/emb.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/emb.con".
-inline cic:/CoRN/metrics/CMetricSpaces/emb_strext.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/emb_strext.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Emb.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Emb.con".
-inline cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con".
(* UNEXPORTED
-End Zeroff.
+End Zeroff
*)
(* UNEXPORTED
-Section Limitt.
+Section Limitt
*)
(*#* **Limit
(* begin hide *)
-inline cic:/CoRN/metrics/CMetricSpaces/nz.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/nz.con".
(* end hide *)
(* begin hide *)
-inline cic:/CoRN/metrics/CMetricSpaces/d_wd.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/d_wd.con".
(* end hide *)
-inline cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con.
+inline "cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con".
(* UNEXPORTED
-End Limitt.
+End Limitt
*)