set "baseuri" "cic:/matita/CoRN-Decl/metrics/CPMSTheory".
+include "CoRN.ma".
+
(* $Id: CPMSTheory.v,v 1.6 2004/04/23 10:01:02 lcf Exp $ *)
-(* INCLUDE
-Prod_Sub
-*)
+include "metrics/Prod_Sub.ma".
(* UNEXPORTED
-Section lists.
+Section lists
*)
(*#* **Lists
the proofs a bit easier.
*)
-inline cic:/CoRN/metrics/CPMSTheory/MSmember.con.
+inline "cic:/CoRN/metrics/CPMSTheory/MSmember.con".
(* UNEXPORTED
Implicit Arguments MSmember [X].
*)
-inline cic:/CoRN/metrics/CPMSTheory/to_IR.con.
+inline "cic:/CoRN/metrics/CPMSTheory/to_IR.con".
-inline cic:/CoRN/metrics/CPMSTheory/from_IR.con.
+inline "cic:/CoRN/metrics/CPMSTheory/from_IR.con".
-inline cic:/CoRN/metrics/CPMSTheory/list_IR.con.
+inline "cic:/CoRN/metrics/CPMSTheory/list_IR.con".
-inline cic:/CoRN/metrics/CPMSTheory/is_P.con.
+inline "cic:/CoRN/metrics/CPMSTheory/is_P.con".
(*#*
If a real number is element of a list in the above defined sense,
that uses the setoid equality.
*)
-inline cic:/CoRN/metrics/CPMSTheory/member1.con.
+inline "cic:/CoRN/metrics/CPMSTheory/member1.con".
(*#*
The image under a certain mapping of an element of a list $l$ #<I>l</I># is member
of the list of images of elements of $l$ #<I>l</I>#.
*)
-inline cic:/CoRN/metrics/CPMSTheory/map_member.con.
+inline "cic:/CoRN/metrics/CPMSTheory/map_member.con".
(* UNEXPORTED
-End lists.
+End lists
*)
(* UNEXPORTED
-Section loc_and_bound.
+Section loc_and_bound
*)
(*#* **Pseudo Metric Space theory
*)
-inline cic:/CoRN/metrics/CPMSTheory/Re_co_do.con.
+inline "cic:/CoRN/metrics/CPMSTheory/Re_co_do.con".
-inline cic:/CoRN/metrics/CPMSTheory/Re_co_do_strext.con.
+inline "cic:/CoRN/metrics/CPMSTheory/Re_co_do_strext.con".
-inline cic:/CoRN/metrics/CPMSTheory/re_co_do.con.
+inline "cic:/CoRN/metrics/CPMSTheory/re_co_do.con".
-inline cic:/CoRN/metrics/CPMSTheory/re_co_do_well_def.con.
+inline "cic:/CoRN/metrics/CPMSTheory/re_co_do_well_def.con".
(* UNEXPORTED
Implicit Arguments MSmember [X].
#<I>l</I># is member of the list of images of elements of $l$ #<I>l</I>#.
*)
-inline cic:/CoRN/metrics/CPMSTheory/map_member'.con.
+inline "cic:/CoRN/metrics/CPMSTheory/map_member'.con".
-inline cic:/CoRN/metrics/CPMSTheory/bounded.con.
+inline "cic:/CoRN/metrics/CPMSTheory/bounded.con".
-inline cic:/CoRN/metrics/CPMSTheory/MStotally_bounded.con.
+inline "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded.con".
(*#*
Total boundedness is preserved under uniformly continuous mappings.
Implicit Arguments SubPsMetricSpace [X].
*)
-inline cic:/CoRN/metrics/CPMSTheory/unicon_resp_totallybounded.con.
+inline "cic:/CoRN/metrics/CPMSTheory/unicon_resp_totallybounded.con".
-inline cic:/CoRN/metrics/CPMSTheory/MStotallybounded_totallybounded.con.
+inline "cic:/CoRN/metrics/CPMSTheory/MStotallybounded_totallybounded.con".
(*#*
Every image under an uniformly continuous function of an totally bounded
pseudo metric space has an infimum and a supremum.
*)
-inline cic:/CoRN/metrics/CPMSTheory/infimum_exists.con.
+inline "cic:/CoRN/metrics/CPMSTheory/infimum_exists.con".
-inline cic:/CoRN/metrics/CPMSTheory/supremum_exists.con.
+inline "cic:/CoRN/metrics/CPMSTheory/supremum_exists.con".
(*#*
A subspace $P$#<I>P</I># of a pseudo metric space $X$#<I>X</I># is said to be located if for all
Implicit Arguments dsub'_as_cs_fun [X].
*)
-inline cic:/CoRN/metrics/CPMSTheory/located.con.
+inline "cic:/CoRN/metrics/CPMSTheory/located.con".
(* UNEXPORTED
Implicit Arguments located [X].
*)
-inline cic:/CoRN/metrics/CPMSTheory/located'.con.
+inline "cic:/CoRN/metrics/CPMSTheory/located'.con".
(* UNEXPORTED
Implicit Arguments located' [X].
*)
-inline cic:/CoRN/metrics/CPMSTheory/located_imp_located'.con.
+inline "cic:/CoRN/metrics/CPMSTheory/located_imp_located'.con".
(*#*
Every totally bounded pseudo metric space is located.
*)
-inline cic:/CoRN/metrics/CPMSTheory/MStotally_bounded_imp_located.con.
+inline "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded_imp_located.con".
(*#*
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>#,
one to use the latter as an argument of [map].
*)
-inline cic:/CoRN/metrics/CPMSTheory/Floc.con.
+inline "cic:/CoRN/metrics/CPMSTheory/Floc.con".
-inline cic:/CoRN/metrics/CPMSTheory/Flocfun.con.
+inline "cic:/CoRN/metrics/CPMSTheory/Flocfun.con".
(*#*
A located subset $P$#<I>P</I># of a totally bounded pseudo metric space $X$
bounded.
*)
-inline cic:/CoRN/metrics/CPMSTheory/locatedsub_totallybounded_imp_totallyboundedsub.con.
+inline "cic:/CoRN/metrics/CPMSTheory/locatedsub_totallybounded_imp_totallyboundedsub.con".
(*#*
Here are some definitions that could come in handy:
*)
-inline cic:/CoRN/metrics/CPMSTheory/MSCauchy_seq.con.
+inline "cic:/CoRN/metrics/CPMSTheory/MSCauchy_seq.con".
(* UNEXPORTED
Implicit Arguments MSseqLimit' [X].
*)
-inline cic:/CoRN/metrics/CPMSTheory/MSComplete.con.
+inline "cic:/CoRN/metrics/CPMSTheory/MSComplete.con".
(*#*
A compact pseudo metric space is a pseudo metric space which is complete and
totally bounded.
*)
-inline cic:/CoRN/metrics/CPMSTheory/MSCompact.con.
+inline "cic:/CoRN/metrics/CPMSTheory/MSCompact.con".
(*#*
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
with centre $x$#<I>x</I># that is contained in $P$#<I>P</I>#.
*)
-inline cic:/CoRN/metrics/CPMSTheory/open.con.
+inline "cic:/CoRN/metrics/CPMSTheory/open.con".
(* UNEXPORTED
Implicit Arguments open [X].
subspace $P$#<I>P</I># of $X$#<I>X</I>#.
*)
-inline cic:/CoRN/metrics/CPMSTheory/infima.con.
+inline "cic:/CoRN/metrics/CPMSTheory/infima.con".
(* UNEXPORTED
Implicit Arguments infima [X].
all points that are in some sense close to $P$#<I>P</I>#.
*)
-inline cic:/CoRN/metrics/CPMSTheory/well_contained.con.
+inline "cic:/CoRN/metrics/CPMSTheory/well_contained.con".
(* UNEXPORTED
-End loc_and_bound.
+End loc_and_bound
*)