(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This file was automatically generated: do not edit *********************) include "CoRN.ma". (* $Id: CPMSTheory.v,v 1.6 2004/04/23 10:01:02 lcf Exp $ *) include "metrics/Prod_Sub.ma". (* UNEXPORTED Section lists *) (*#* **Lists *) (*#* List and membership of lists are used in the definition of %''totally bounded''% #"totally bounded"#. Note that we use the Leibniz equality in the definition of [MSmember], and not the setoid equality. So we are really talking about finite sets of representants, instead of finite subsetoids. This seems to make the proofs a bit easier. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/MSmember.con" as definition. (* UNEXPORTED Implicit Arguments MSmember [X]. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/to_IR.con" as definition. inline procedural "cic:/CoRN/metrics/CPMSTheory/from_IR.con" as definition. inline procedural "cic:/CoRN/metrics/CPMSTheory/list_IR.con" as definition. inline procedural "cic:/CoRN/metrics/CPMSTheory/is_P.con" as lemma. (*#* If a real number is element of a list in the above defined sense, it is an element of the list in the sense of [member], that uses the setoid equality. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/member1.con" as lemma. (*#* The image under a certain mapping of an element of a list $l$ #l# is member of the list of images of elements of $l$ #l#. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/map_member.con" as lemma. (* UNEXPORTED End lists *) (* UNEXPORTED Section loc_and_bound *) (*#* **Pseudo Metric Space theory *) inline procedural "cic:/CoRN/metrics/CPMSTheory/Re_co_do.con" as definition. inline procedural "cic:/CoRN/metrics/CPMSTheory/Re_co_do_strext.con" as lemma. inline procedural "cic:/CoRN/metrics/CPMSTheory/re_co_do.con" as definition. inline procedural "cic:/CoRN/metrics/CPMSTheory/re_co_do_well_def.con" as lemma. (* UNEXPORTED Implicit Arguments MSmember [X]. *) (*#* Again we see that the image under a certain mapping of an element of a list $l$ #l# is member of the list of images of elements of $l$ #l#. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/map_member'.con" as lemma. inline procedural "cic:/CoRN/metrics/CPMSTheory/bounded.con" as definition. inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded.con" as definition. (*#* Total boundedness is preserved under uniformly continuous mappings. *) (* UNEXPORTED Implicit Arguments SubPsMetricSpace [X]. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/unicon_resp_totallybounded.con" as lemma. inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotallybounded_totallybounded.con" as lemma. (*#* Every image under an uniformly continuous function of an totally bounded pseudo metric space has an infimum and a supremum. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/infimum_exists.con" as lemma. inline procedural "cic:/CoRN/metrics/CPMSTheory/supremum_exists.con" as lemma. (*#* A subspace $P$#P# of a pseudo metric space $X$#X# is said to be located if for all elements $x$#x# of $X$#X# there exists an infimum for the distance between $x$#x# and the elements of $P$#P#. *) (* UNEXPORTED Implicit Arguments dsub'_as_cs_fun [X]. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/located.con" as definition. (* UNEXPORTED Implicit Arguments located [X]. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/located'.con" as definition. (* UNEXPORTED Implicit Arguments located' [X]. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/located_imp_located'.con" as lemma. (*#* Every totally bounded pseudo metric space is located. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded_imp_located.con" as lemma. (*#* For all $x$#x# in a pseudo metric space $X$#X#, for all located subspaces $P$#P# of $X$#X#, [Floc] chooses for a given natural number $n$#n# an $y$#y# in $P$#P# such that: $d(x,y)\leq \mbox{inf}\{d(x,p)|p \in P\}+(n+1)^{-1}$ #d(x,y) ≤ inf{d(x,p)| pϵP} + (n+1)-1#. [Flocfun] does (almost) the same, but has a different type. This enables one to use the latter as an argument of [map]. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/Floc.con" as definition. inline procedural "cic:/CoRN/metrics/CPMSTheory/Flocfun.con" as definition. (*#* A located subset $P$#P# of a totally bounded pseudo metric space $X$ #X# is totally bounded. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/locatedsub_totallybounded_imp_totallyboundedsub.con" as lemma. (*#* Here are some definitions that could come in handy: *) inline procedural "cic:/CoRN/metrics/CPMSTheory/MSCauchy_seq.con" as definition. (* UNEXPORTED Implicit Arguments MSseqLimit' [X]. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/MSComplete.con" as definition. (*#* A compact pseudo metric space is a pseudo metric space which is complete and totally bounded. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/MSCompact.con" as definition. (*#* A subset $P$#P# is %\emph{open}%#open# if for all $x$#x# in $P$#P# there exists an open sphere with centre $x$#x# that is contained in $P$#P#. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/open.con" as definition. (* UNEXPORTED Implicit Arguments open [X]. *) (*#* The operator [infima] gives the infimum for the distance between an element $x$#x# of a located pseudo metric space $X$#X# and the elements of a subspace $P$#P# of $X$#X#. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/infima.con" as definition. (* UNEXPORTED Implicit Arguments infima [X]. *) (*#* A non-empty totally bounded sub-pseudo-metric-space $P$#P# is said to be %\emph{well contained}% #well contained# in an open sub-pseudo-metric-space $Q$#Q# if $Q$#Q# contains all points that are in some sense close to $P$#P#. *) inline procedural "cic:/CoRN/metrics/CPMSTheory/well_contained.con" as definition. (* UNEXPORTED End loc_and_bound *)