....

[helm.git] / helm / software / matita / contribs / CoRN-Decl / metrics / CMetricSpaces.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
index 7996af4961002b7f55f93ea3a09a7d9e8e36da46..45f6ff0c6e98416aba0c5c1878da32aad358db4d 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
@@ -16,48 +16,48 @@
 
 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
@@ -67,9 +67,9 @@ Section prodandsub.
 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.
@@ -79,20 +79,20 @@ 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
@@ -102,76 +102,76 @@ Section Zeroff.
 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
@@ -187,19 +187,19 @@ Implicit Arguments MSseqLimit [X].
 
 (* 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
 *)