(**************************************************************************)
(* ___ *)
(* ||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
*)