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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/metrics/CPMSTheory".
19 (* $Id: CPMSTheory.v,v 1.6 2004/04/23 10:01:02 lcf Exp $ *)
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.
40 inline cic:/CoRN/metrics/CPMSTheory/MSmember.con.
43 Implicit Arguments MSmember [X].
46 inline cic:/CoRN/metrics/CPMSTheory/to_IR.con.
48 inline cic:/CoRN/metrics/CPMSTheory/from_IR.con.
50 inline cic:/CoRN/metrics/CPMSTheory/list_IR.con.
52 inline cic:/CoRN/metrics/CPMSTheory/is_P.con.
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.
60 inline cic:/CoRN/metrics/CPMSTheory/member1.con.
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>#.
67 inline cic:/CoRN/metrics/CPMSTheory/map_member.con.
74 Section loc_and_bound.
77 (*#* **Pseudo Metric Space theory
80 inline cic:/CoRN/metrics/CPMSTheory/Re_co_do.con.
82 inline cic:/CoRN/metrics/CPMSTheory/Re_co_do_strext.con.
84 inline cic:/CoRN/metrics/CPMSTheory/re_co_do.con.
86 inline cic:/CoRN/metrics/CPMSTheory/re_co_do_well_def.con.
89 Implicit Arguments MSmember [X].
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>#.
97 inline cic:/CoRN/metrics/CPMSTheory/map_member'.con.
99 inline cic:/CoRN/metrics/CPMSTheory/bounded.con.
101 inline cic:/CoRN/metrics/CPMSTheory/MStotally_bounded.con.
104 Total boundedness is preserved under uniformly continuous mappings.
108 Implicit Arguments SubPsMetricSpace [X].
111 inline cic:/CoRN/metrics/CPMSTheory/unicon_resp_totallybounded.con.
113 inline cic:/CoRN/metrics/CPMSTheory/MStotallybounded_totallybounded.con.
116 Every image under an uniformly continuous function of an totally bounded
117 pseudo metric space has an infimum and a supremum.
120 inline cic:/CoRN/metrics/CPMSTheory/infimum_exists.con.
122 inline cic:/CoRN/metrics/CPMSTheory/supremum_exists.con.
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>#.
131 Implicit Arguments dsub'_as_cs_fun [X].
134 inline cic:/CoRN/metrics/CPMSTheory/located.con.
137 Implicit Arguments located [X].
140 inline cic:/CoRN/metrics/CPMSTheory/located'.con.
143 Implicit Arguments located' [X].
146 inline cic:/CoRN/metrics/CPMSTheory/located_imp_located'.con.
149 Every totally bounded pseudo metric space is located.
152 inline cic:/CoRN/metrics/CPMSTheory/MStotally_bounded_imp_located.con.
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) ≤ inf{d(x,p)| pϵP} + (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].
163 inline cic:/CoRN/metrics/CPMSTheory/Floc.con.
165 inline cic:/CoRN/metrics/CPMSTheory/Flocfun.con.
168 A located subset $P$#<I>P</I># of a totally bounded pseudo metric space $X$
169 #<I>X</I># is totally
173 inline cic:/CoRN/metrics/CPMSTheory/locatedsub_totallybounded_imp_totallyboundedsub.con.
176 Here are some definitions that could come in handy:
179 inline cic:/CoRN/metrics/CPMSTheory/MSCauchy_seq.con.
182 Implicit Arguments MSseqLimit' [X].
185 inline cic:/CoRN/metrics/CPMSTheory/MSComplete.con.
188 A compact pseudo metric space is a pseudo metric space which is complete and
192 inline cic:/CoRN/metrics/CPMSTheory/MSCompact.con.
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>#.
199 inline cic:/CoRN/metrics/CPMSTheory/open.con.
202 Implicit Arguments open [X].
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>#.
211 inline cic:/CoRN/metrics/CPMSTheory/infima.con.
214 Implicit Arguments infima [X].
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>#.
223 inline cic:/CoRN/metrics/CPMSTheory/well_contained.con.