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: CPMSTheory.v,v 1.6 2004/04/23 10:01:02 lcf Exp $ *)
21 include "metrics/Prod_Sub.ma".
31 List and membership of lists are used in the definition of
32 %''totally bounded''% #"totally bounded"#. Note that we use the Leibniz equality in the definition
33 of [MSmember], and not the setoid equality. So we are really talking about
34 finite sets of representants, instead of finite subsetoids. This seems to make
35 the proofs a bit easier.
38 inline procedural "cic:/CoRN/metrics/CPMSTheory/MSmember.con" as definition.
41 Implicit Arguments MSmember [X].
44 inline procedural "cic:/CoRN/metrics/CPMSTheory/to_IR.con" as definition.
46 inline procedural "cic:/CoRN/metrics/CPMSTheory/from_IR.con" as definition.
48 inline procedural "cic:/CoRN/metrics/CPMSTheory/list_IR.con" as definition.
50 inline procedural "cic:/CoRN/metrics/CPMSTheory/is_P.con" as lemma.
53 If a real number is element of a list in the above defined sense,
54 it is an element of the list in the sense of [member],
55 that uses the setoid equality.
58 inline procedural "cic:/CoRN/metrics/CPMSTheory/member1.con" as lemma.
61 The image under a certain mapping of an element of a list $l$ #<I>l</I># is member
62 of the list of images of elements of $l$ #<I>l</I>#.
65 inline procedural "cic:/CoRN/metrics/CPMSTheory/map_member.con" as lemma.
75 (*#* **Pseudo Metric Space theory
78 inline procedural "cic:/CoRN/metrics/CPMSTheory/Re_co_do.con" as definition.
80 inline procedural "cic:/CoRN/metrics/CPMSTheory/Re_co_do_strext.con" as lemma.
82 inline procedural "cic:/CoRN/metrics/CPMSTheory/re_co_do.con" as definition.
84 inline procedural "cic:/CoRN/metrics/CPMSTheory/re_co_do_well_def.con" as lemma.
87 Implicit Arguments MSmember [X].
91 Again we see that the image under a certain mapping of an element of a list $l$
92 #<I>l</I># is member of the list of images of elements of $l$ #<I>l</I>#.
95 inline procedural "cic:/CoRN/metrics/CPMSTheory/map_member'.con" as lemma.
97 inline procedural "cic:/CoRN/metrics/CPMSTheory/bounded.con" as definition.
99 inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded.con" as definition.
102 Total boundedness is preserved under uniformly continuous mappings.
106 Implicit Arguments SubPsMetricSpace [X].
109 inline procedural "cic:/CoRN/metrics/CPMSTheory/unicon_resp_totallybounded.con" as lemma.
111 inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotallybounded_totallybounded.con" as lemma.
114 Every image under an uniformly continuous function of an totally bounded
115 pseudo metric space has an infimum and a supremum.
118 inline procedural "cic:/CoRN/metrics/CPMSTheory/infimum_exists.con" as lemma.
120 inline procedural "cic:/CoRN/metrics/CPMSTheory/supremum_exists.con" as lemma.
123 A subspace $P$#<I>P</I># of a pseudo metric space $X$#<I>X</I># is said to be located if for all
124 elements $x$#<I>x</I># of $X$#<I>X</I># there exists an infimum for the distance
125 between $x$#<I>x</I># and the elements of $P$#<I>P</I>#.
129 Implicit Arguments dsub'_as_cs_fun [X].
132 inline procedural "cic:/CoRN/metrics/CPMSTheory/located.con" as definition.
135 Implicit Arguments located [X].
138 inline procedural "cic:/CoRN/metrics/CPMSTheory/located'.con" as definition.
141 Implicit Arguments located' [X].
144 inline procedural "cic:/CoRN/metrics/CPMSTheory/located_imp_located'.con" as lemma.
147 Every totally bounded pseudo metric space is located.
150 inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded_imp_located.con" as lemma.
153 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>#,
154 [Floc] chooses for a given natural number $n$#<I>n</I># an $y$#<I>y</I># in $P$#<I>P</I># such that:
155 $d(x,y)\leq \mbox{inf}\{d(x,p)|p \in P\}+(n+1)^{-1}$
156 #d(x,y) ≤ inf{d(x,p)| pϵP} + (n+1)<SUP>-1</SUP>#.
157 [Flocfun] does (almost) the same, but has a different type. This enables
158 one to use the latter as an argument of [map].
161 inline procedural "cic:/CoRN/metrics/CPMSTheory/Floc.con" as definition.
163 inline procedural "cic:/CoRN/metrics/CPMSTheory/Flocfun.con" as definition.
166 A located subset $P$#<I>P</I># of a totally bounded pseudo metric space $X$
167 #<I>X</I># is totally
171 inline procedural "cic:/CoRN/metrics/CPMSTheory/locatedsub_totallybounded_imp_totallyboundedsub.con" as lemma.
174 Here are some definitions that could come in handy:
177 inline procedural "cic:/CoRN/metrics/CPMSTheory/MSCauchy_seq.con" as definition.
180 Implicit Arguments MSseqLimit' [X].
183 inline procedural "cic:/CoRN/metrics/CPMSTheory/MSComplete.con" as definition.
186 A compact pseudo metric space is a pseudo metric space which is complete and
190 inline procedural "cic:/CoRN/metrics/CPMSTheory/MSCompact.con" as definition.
193 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
194 with centre $x$#<I>x</I># that is contained in $P$#<I>P</I>#.
197 inline procedural "cic:/CoRN/metrics/CPMSTheory/open.con" as definition.
200 Implicit Arguments open [X].
204 The operator [infima] gives the infimum for the distance between an
205 element $x$#<I>x</I># of a located pseudo metric space $X$#<I>X</I># and the elements of a
206 subspace $P$#<I>P</I># of $X$#<I>X</I>#.
209 inline procedural "cic:/CoRN/metrics/CPMSTheory/infima.con" as definition.
212 Implicit Arguments infima [X].
216 A non-empty totally bounded sub-pseudo-metric-space $P$#<I>P</I># is said to be
217 %\emph{well contained}% #<I>well contained</I># in an open sub-pseudo-metric-space $Q$#<I>Q</I># if $Q$#<I>Q</I># contains
218 all points that are in some sense close to $P$#<I>P</I>#.
221 inline procedural "cic:/CoRN/metrics/CPMSTheory/well_contained.con" as definition.