X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Procedural%2Fmetrics%2FCMetricSpaces.mma;h=b0d848ec0246f831cab9ad5eb41c30b2e698503a;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=670bf8655fc36193e9ccdf4b5d0942e04157df4c;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Procedural/metrics/CMetricSpaces.mma b/helm/software/matita/contribs/CoRN-Procedural/metrics/CMetricSpaces.mma index 670bf8655..b0d848ec0 100644 --- a/helm/software/matita/contribs/CoRN-Procedural/metrics/CMetricSpaces.mma +++ b/helm/software/matita/contribs/CoRN-Procedural/metrics/CMetricSpaces.mma @@ -46,11 +46,11 @@ Section MS_basics (*#* **Metric Space basics *) -inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_CMetricSpace_apdiag_imp_grzero.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_CMetricSpace_apdiag_imp_grzero.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con" as lemma. (* UNEXPORTED End MS_basics @@ -67,9 +67,9 @@ Section prodandsub The product of two metric spaces is again a metric space. *) -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpaces_apdiag_grzero.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpaces_apdiag_grzero.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpace.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpace.con" as definition. (*#* 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 procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace_apdiag_grzero.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace_apdiag_grzero.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace.con" as definition. (* UNEXPORTED Implicit Arguments SubMetricSpace [X]. @@ -102,69 +102,69 @@ Section Zeroff Not all pseudo metric spaces are a metric space: *) -inline procedural "cic:/CoRN/metrics/CMetricSpaces/zf_nis_CMetricSpace.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/zf_nis_CMetricSpace.con" as lemma. (*#* But a pseudo metric space induces a metric space: *) -inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap.con" as definition. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_eq.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_eq.con" as definition. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_irreflexive.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_irreflexive.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_symmetric.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_symmetric.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_cotransitive.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_cotransitive.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_tight.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_tight.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSet_is_CSetoid.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSet_is_CSetoid.con" as definition. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSetoid.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSetoid.con" as definition. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d.con" as definition. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d_strext.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d_strext.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d.con" as definition. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_com.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_com.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_nneg.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_nneg.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_pos_imp_ap.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_pos_imp_ap.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_tri_ineq.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_tri_ineq.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCSetoid_is_CPsMetricSpace.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCSetoid_is_CPsMetricSpace.con" as definition. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCPsMetricSpace.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCPsMetricSpace.con" as definition. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_apdiag_grzero.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_apdiag_grzero.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCMetricSpace.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCMetricSpace.con" as definition. (*#* Some pseudo metric spaces already are a metric space: *) -inline procedural "cic:/CoRN/metrics/CMetricSpaces/dIR_apdiag_grzero.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/dIR_apdiag_grzero.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/IR_as_CMetricSpace.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/IR_as_CMetricSpace.con" as definition. (*#* In that case the induced metric space is equivalent to the original one: *) -inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb.con" as definition. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb_strext.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb_strext.con" as lemma. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Emb.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Emb.con" as definition. -inline procedural "cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con" as lemma. (* UNEXPORTED End Zeroff @@ -187,17 +187,17 @@ Implicit Arguments MSseqLimit [X]. (* begin hide *) -inline procedural "cic:/CoRN/metrics/CMetricSpaces/nz.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/nz.con" as lemma. (* end hide *) (* begin hide *) -inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_wd.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_wd.con" as lemma. (* end hide *) -inline procedural "cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con". +inline procedural "cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con" as lemma. (* UNEXPORTED End Limitt