1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: CMetricSpaces.v,v 1.4 2004/04/23 10:01:01 lcf Exp $ *)
21 include "metrics/Prod_Sub.ma".
23 include "metrics/Equiv.ma".
29 (*#* **Definition of Metric Space
32 inline procedural "cic:/CoRN/metrics/CMetricSpaces/CMetricSpace.ind".
35 cic:/matita/CoRN-Procedural/metrics/CMetricSpaces/scms_crr.con
46 (*#* **Metric Space basics
49 inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_CMetricSpace_apdiag_imp_grzero.con" as lemma.
51 inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con" as lemma.
53 inline procedural "cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con" as lemma.
63 (*#* **Product-Metric-Spaces and Sub-Metric-Spaces
67 The product of two metric spaces is again a metric space.
70 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpaces_apdiag_grzero.con" as lemma.
72 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpace.con" as definition.
75 A subspace of a metric space is again a metric space.
79 Implicit Arguments SubPsMetricSpace [X].
82 inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace_apdiag_grzero.con" as lemma.
84 inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace.con" as definition.
87 Implicit Arguments SubMetricSpace [X].
98 (*#* **Pseudo Metric Spaces vs Metric Spaces
102 Not all pseudo metric spaces are a metric space:
105 inline procedural "cic:/CoRN/metrics/CMetricSpaces/zf_nis_CMetricSpace.con" as lemma.
108 But a pseudo metric space induces a metric space:
111 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap.con" as definition.
113 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_eq.con" as definition.
115 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_irreflexive.con" as lemma.
117 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_symmetric.con" as lemma.
119 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_cotransitive.con" as lemma.
121 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_tight.con" as lemma.
123 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSet_is_CSetoid.con" as definition.
125 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSetoid.con" as definition.
127 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d.con" as definition.
129 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d_strext.con" as lemma.
131 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d.con" as definition.
133 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_com.con" as lemma.
135 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_nneg.con" as lemma.
137 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_pos_imp_ap.con" as lemma.
139 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_tri_ineq.con" as lemma.
141 inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCSetoid_is_CPsMetricSpace.con" as definition.
143 inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCPsMetricSpace.con" as definition.
145 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_apdiag_grzero.con" as lemma.
147 inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCMetricSpace.con" as definition.
150 Some pseudo metric spaces already are a metric space:
153 inline procedural "cic:/CoRN/metrics/CMetricSpaces/dIR_apdiag_grzero.con" as lemma.
155 inline procedural "cic:/CoRN/metrics/CMetricSpaces/IR_as_CMetricSpace.con" as definition.
158 In that case the induced metric space is equivalent to the original one:
161 inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb.con" as definition.
163 inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb_strext.con" as lemma.
165 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Emb.con" as definition.
167 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con" as lemma.
181 A sequence in a metric space has at most one limit.
185 Implicit Arguments MSseqLimit [X].
190 inline procedural "cic:/CoRN/metrics/CMetricSpaces/nz.con" as lemma.
196 inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_wd.con" as lemma.
200 inline procedural "cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con" as lemma.