X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FCMetricSpaces.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FCMetricSpaces.ma;h=3b0591a8028ea9601b1bee1af4305aefd7d99916;hb=80110e17ef1d38d71473e9471ce15beddde663bb;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..3b0591a80 100644 --- a/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma +++ b/helm/software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma @@ -16,15 +16,13 @@ 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. @@ -33,7 +31,9 @@ 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. @@ -46,11 +46,11 @@ 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. @@ -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,9 +79,9 @@ 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]. @@ -102,69 +102,69 @@ 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. @@ -187,17 +187,17 @@ 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.