]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
two cases of cpx_lfxs_conf_fle closed
[helm.git] / matita / matita / contribs / CoRN-Decl / metrics / CPMSTheory.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/CPMSTheory".
18
19 include "CoRN.ma".
20
21 (* $Id: CPMSTheory.v,v 1.6 2004/04/23 10:01:02 lcf Exp $ *)
22
23 include "metrics/Prod_Sub.ma".
24
25 (* UNEXPORTED
26 Section lists
27 *)
28
29 (*#* **Lists
30 *)
31
32 (*#*
33  List and membership of lists are used in the definition of 
34 %''totally bounded''% #"totally bounded"#. Note that we use the Leibniz equality in the definition 
35 of [MSmember], and not the setoid equality. So we are really talking about
36 finite sets of representants, instead of finite subsetoids. This seems to make
37  the proofs a bit easier.
38 *)
39
40 inline "cic:/CoRN/metrics/CPMSTheory/MSmember.con".
41
42 (* UNEXPORTED
43 Implicit Arguments MSmember [X].
44 *)
45
46 inline "cic:/CoRN/metrics/CPMSTheory/to_IR.con".
47
48 inline "cic:/CoRN/metrics/CPMSTheory/from_IR.con".
49
50 inline "cic:/CoRN/metrics/CPMSTheory/list_IR.con".
51
52 inline "cic:/CoRN/metrics/CPMSTheory/is_P.con".
53
54 (*#*
55 If a real number is element of a list in the above defined sense,
56 it is an element of the list in the sense of [member], 
57 that uses the setoid equality.
58 *)
59
60 inline "cic:/CoRN/metrics/CPMSTheory/member1.con".
61
62 (*#*
63 The image under a certain mapping of an element of a list $l$ #<I>l</I># is member 
64 of the list of images of elements of $l$ #<I>l</I>#.
65 *)
66
67 inline "cic:/CoRN/metrics/CPMSTheory/map_member.con".
68
69 (* UNEXPORTED
70 End lists
71 *)
72
73 (* UNEXPORTED
74 Section loc_and_bound
75 *)
76
77 (*#* **Pseudo Metric Space theory
78 *)
79
80 inline "cic:/CoRN/metrics/CPMSTheory/Re_co_do.con".
81
82 inline "cic:/CoRN/metrics/CPMSTheory/Re_co_do_strext.con".
83
84 inline "cic:/CoRN/metrics/CPMSTheory/re_co_do.con".
85
86 inline "cic:/CoRN/metrics/CPMSTheory/re_co_do_well_def.con".
87
88 (* UNEXPORTED
89 Implicit Arguments MSmember [X].
90 *)
91
92 (*#*
93 Again we see that the image under a certain mapping of an element of a list $l$
94 #<I>l</I># is member of the list of images of elements of $l$ #<I>l</I>#.
95 *)
96
97 inline "cic:/CoRN/metrics/CPMSTheory/map_member'.con".
98
99 inline "cic:/CoRN/metrics/CPMSTheory/bounded.con".
100
101 inline "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded.con".
102
103 (*#*
104 Total boundedness is preserved under uniformly continuous mappings.
105 *)
106
107 (* UNEXPORTED
108 Implicit Arguments SubPsMetricSpace [X].
109 *)
110
111 inline "cic:/CoRN/metrics/CPMSTheory/unicon_resp_totallybounded.con".
112
113 inline "cic:/CoRN/metrics/CPMSTheory/MStotallybounded_totallybounded.con".
114
115 (*#*
116 Every image under an uniformly continuous function of an totally bounded 
117 pseudo metric space has an infimum and a supremum.
118 *)
119
120 inline "cic:/CoRN/metrics/CPMSTheory/infimum_exists.con".
121
122 inline "cic:/CoRN/metrics/CPMSTheory/supremum_exists.con".
123
124 (*#*
125 A subspace $P$#<I>P</I># of a pseudo metric space $X$#<I>X</I># is said to be located if for all 
126 elements $x$#<I>x</I># of $X$#<I>X</I># there exists an infimum for the distance 
127 between $x$#<I>x</I># and the elements of $P$#<I>P</I>#.
128 *)
129
130 (* UNEXPORTED
131 Implicit Arguments dsub'_as_cs_fun [X].
132 *)
133
134 inline "cic:/CoRN/metrics/CPMSTheory/located.con".
135
136 (* UNEXPORTED
137 Implicit Arguments located [X].
138 *)
139
140 inline "cic:/CoRN/metrics/CPMSTheory/located'.con".
141
142 (* UNEXPORTED
143 Implicit Arguments located' [X].
144 *)
145
146 inline "cic:/CoRN/metrics/CPMSTheory/located_imp_located'.con".
147
148 (*#*
149 Every totally bounded pseudo metric space is located.
150 *)
151
152 inline "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded_imp_located.con".
153
154 (*#*
155 For all $x$#<I>x</I># in a pseudo metric space $X$#<I>X</I>#, for all located subspaces $P$#<I>P</I># of $X$#<I>X</I>#,
156 [Floc] chooses for a given natural number $n$#<I>n</I># an $y$#<I>y</I># in $P$#<I>P</I># such that:
157 $d(x,y)\leq \mbox{inf}\{d(x,p)|p \in P\}+(n+1)^{-1}$
158 #d(x,y) &le; inf&#x007B;d(x,p)&#x007C; p&#x03F5;P&#x007D; + (n+1)<SUP>-1</SUP>#.
159 [Flocfun] does (almost) the same, but has a different type. This enables 
160 one to use the latter as an argument of [map].
161 *)
162
163 inline "cic:/CoRN/metrics/CPMSTheory/Floc.con".
164
165 inline "cic:/CoRN/metrics/CPMSTheory/Flocfun.con".
166
167 (*#*
168 A located subset $P$#<I>P</I># of a totally bounded pseudo metric space $X$
169 #<I>X</I># is totally
170 bounded.
171 *)
172
173 inline "cic:/CoRN/metrics/CPMSTheory/locatedsub_totallybounded_imp_totallyboundedsub.con".
174
175 (*#*
176 Here are some definitions that could come in handy:
177 *)
178
179 inline "cic:/CoRN/metrics/CPMSTheory/MSCauchy_seq.con".
180
181 (* UNEXPORTED
182 Implicit Arguments MSseqLimit' [X].
183 *)
184
185 inline "cic:/CoRN/metrics/CPMSTheory/MSComplete.con".
186
187 (*#*
188 A compact pseudo metric space is a pseudo metric space which is complete and 
189 totally bounded.
190 *)
191
192 inline "cic:/CoRN/metrics/CPMSTheory/MSCompact.con".
193
194 (*#*
195 A subset $P$#<I>P</I># is %\emph{open}%#<I>open</I># if for all $x$#<I>x</I># in $P$#<I>P</I># there exists an open sphere 
196 with centre $x$#<I>x</I># that is contained in $P$#<I>P</I>#.
197 *)
198
199 inline "cic:/CoRN/metrics/CPMSTheory/open.con".
200
201 (* UNEXPORTED
202 Implicit Arguments open [X].
203 *)
204
205 (*#*
206 The operator [infima] gives the infimum for the distance between an 
207 element $x$#<I>x</I># of a located pseudo metric space $X$#<I>X</I># and the elements of a 
208 subspace $P$#<I>P</I># of $X$#<I>X</I>#.
209 *)
210
211 inline "cic:/CoRN/metrics/CPMSTheory/infima.con".
212
213 (* UNEXPORTED
214 Implicit Arguments infima [X].
215 *)
216
217 (*#*
218 A non-empty totally bounded sub-pseudo-metric-space $P$#<I>P</I># is said to be 
219 %\emph{well contained}% #<I>well contained</I># in an open sub-pseudo-metric-space $Q$#<I>Q</I># if $Q$#<I>Q</I># contains 
220 all points that are in some sense close to $P$#<I>P</I>#.
221 *)
222
223 inline "cic:/CoRN/metrics/CPMSTheory/well_contained.con".
224
225 (* UNEXPORTED
226 End loc_and_bound
227 *)
228