]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
librarySync - we do not generate the object attributes when we publish the xml
[helm.git] / matita / contribs / CoRN-Decl / metrics / CMetricSpaces.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 set "baseuri" "cic:/matita/CoRN-Decl/metrics/CMetricSpaces".
18
19 include "CoRN.ma".
20
21 (* $Id: CMetricSpaces.v,v 1.4 2004/04/23 10:01:01 lcf Exp $ *)
22
23 include "metrics/Prod_Sub.ma".
24
25 include "metrics/Equiv.ma".
26
27 (* UNEXPORTED
28 Section Definition_MS
29 *)
30
31 (*#* **Definition of Metric Space
32 *)
33
34 inline "cic:/CoRN/metrics/CMetricSpaces/CMetricSpace.ind".
35
36 coercion cic:/matita/CoRN-Decl/metrics/CMetricSpaces/scms_crr.con 0 (* compounds *).
37
38 (* UNEXPORTED
39 End Definition_MS
40 *)
41
42 (* UNEXPORTED
43 Section MS_basics
44 *)
45
46 (*#* **Metric Space basics
47 *)
48
49 inline "cic:/CoRN/metrics/CMetricSpaces/d_CMetricSpace_apdiag_imp_grzero.con".
50
51 inline "cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con".
52
53 inline "cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con".
54
55 (* UNEXPORTED
56 End MS_basics
57 *)
58
59 (* UNEXPORTED
60 Section prodandsub
61 *)
62
63 (*#* **Product-Metric-Spaces and Sub-Metric-Spaces
64 *)
65
66 (*#*
67 The product of two metric spaces is again a metric space.
68 *)
69
70 inline "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpaces_apdiag_grzero.con".
71
72 inline "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpace.con".
73
74 (*#*
75 A subspace of a metric space is again a metric space.
76 *)
77
78 (* UNEXPORTED
79 Implicit Arguments SubPsMetricSpace [X].
80 *)
81
82 inline "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace_apdiag_grzero.con".
83
84 inline "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace.con".
85
86 (* UNEXPORTED
87 Implicit Arguments SubMetricSpace [X].
88 *)
89
90 (* UNEXPORTED
91 End prodandsub
92 *)
93
94 (* UNEXPORTED
95 Section Zeroff
96 *)
97
98 (*#* **Pseudo Metric Spaces vs Metric Spaces
99 *)
100
101 (*#*
102 Not all pseudo metric spaces are a metric space:
103 *)
104
105 inline "cic:/CoRN/metrics/CMetricSpaces/zf_nis_CMetricSpace.con".
106
107 (*#*
108 But a pseudo metric space induces a metric space:
109 *)
110
111 inline "cic:/CoRN/metrics/CMetricSpaces/metric_ap.con".
112
113 inline "cic:/CoRN/metrics/CMetricSpaces/metric_eq.con".
114
115 inline "cic:/CoRN/metrics/CMetricSpaces/metric_ap_irreflexive.con".
116
117 inline "cic:/CoRN/metrics/CMetricSpaces/metric_ap_symmetric.con".
118
119 inline "cic:/CoRN/metrics/CMetricSpaces/metric_ap_cotransitive.con".
120
121 inline "cic:/CoRN/metrics/CMetricSpaces/metric_ap_tight.con".
122
123 inline "cic:/CoRN/metrics/CMetricSpaces/Metric_CSet_is_CSetoid.con".
124
125 inline "cic:/CoRN/metrics/CMetricSpaces/Metric_CSetoid.con".
126
127 inline "cic:/CoRN/metrics/CMetricSpaces/metric_d.con".
128
129 inline "cic:/CoRN/metrics/CMetricSpaces/metric_d_strext.con".
130
131 inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d.con".
132
133 inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d_com.con".
134
135 inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d_nneg.con".
136
137 inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d_pos_imp_ap.con".
138
139 inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d_tri_ineq.con".
140
141 inline "cic:/CoRN/metrics/CMetricSpaces/QuotientCSetoid_is_CPsMetricSpace.con".
142
143 inline "cic:/CoRN/metrics/CMetricSpaces/QuotientCPsMetricSpace.con".
144
145 inline "cic:/CoRN/metrics/CMetricSpaces/Metric_d_apdiag_grzero.con".
146
147 inline "cic:/CoRN/metrics/CMetricSpaces/QuotientCMetricSpace.con".
148
149 (*#*
150 Some pseudo metric spaces already are a metric space:
151 *)
152
153 inline "cic:/CoRN/metrics/CMetricSpaces/dIR_apdiag_grzero.con".
154
155 inline "cic:/CoRN/metrics/CMetricSpaces/IR_as_CMetricSpace.con".
156
157 (*#*
158 In that case the induced metric space is equivalent to the original one:
159 *)
160
161 inline "cic:/CoRN/metrics/CMetricSpaces/emb.con".
162
163 inline "cic:/CoRN/metrics/CMetricSpaces/emb_strext.con".
164
165 inline "cic:/CoRN/metrics/CMetricSpaces/Emb.con".
166
167 inline "cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con".
168
169 (* UNEXPORTED
170 End Zeroff
171 *)
172
173 (* UNEXPORTED
174 Section Limitt
175 *)
176
177 (*#* **Limit
178 *)
179
180 (*#*
181 A sequence in a metric space has at most one limit.
182 *)
183
184 (* UNEXPORTED
185 Implicit Arguments MSseqLimit [X].
186 *)
187
188 (* begin hide *)
189
190 inline "cic:/CoRN/metrics/CMetricSpaces/nz.con".
191
192 (* end hide *)
193
194 (* begin hide *)
195
196 inline "cic:/CoRN/metrics/CMetricSpaces/d_wd.con".
197
198 (* end hide *)
199
200 inline "cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con".
201
202 (* UNEXPORTED
203 End Limitt
204 *)
205