X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FCMetricSpaces.ma;h=45f6ff0c6e98416aba0c5c1878da32aad358db4d;hb=3cf6181bded05eb63140d1b2ba4f2f5791a73b48;hp=7996af4961002b7f55f93ea3a09a7d9e8e36da46;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma index 7996af496..45f6ff0c6 100644 --- 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 *)