X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fmetrics%2FCPMSTheory.ma;h=50786005f33f637bcf1b1e2dedeb9d39df2b0552;hb=11e495dda047bcdfa4267c06cad2d074fcffe3e3;hp=fe04f4fb1121618cc6e78c7d8b6344af2e33ba47;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git
diff --git a/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma b/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
index fe04f4fb1..50786005f 100644
--- a/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
@@ -16,14 +16,14 @@
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
@@ -37,19 +37,19 @@ finite sets of representants, instead of finite subsetoids. This seems to make
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,
@@ -57,33 +57,33 @@ it is an element of the list in the sense of [member],
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$ #l# is member
of the list of images of elements of $l$ #l#.
*)
-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].
@@ -94,11 +94,11 @@ 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 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.
@@ -108,18 +108,18 @@ 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$#P# of a pseudo metric space $X$#X# is said to be located if for all
@@ -131,25 +131,25 @@ between $x$#x# and the elements of $P$#P#.
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$#x# in a pseudo metric space $X$#X#, for all located subspaces $P$#P# of $X$#X#,
@@ -160,9 +160,9 @@ $d(x,y)\leq \mbox{inf}\{d(x,p)|p \in P\}+(n+1)^{-1}$
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$#P# of a totally bounded pseudo metric space $X$
@@ -170,33 +170,33 @@ A located subset $P$#P# 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$#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 cic:/CoRN/metrics/CPMSTheory/open.con.
+inline "cic:/CoRN/metrics/CPMSTheory/open.con".
(* UNEXPORTED
Implicit Arguments open [X].
@@ -208,7 +208,7 @@ element $x$#x# of a located pseudo metric space $X$#X# and the ele
subspace $P$#P# of $X$#X#.
*)
-inline cic:/CoRN/metrics/CPMSTheory/infima.con.
+inline "cic:/CoRN/metrics/CPMSTheory/infima.con".
(* UNEXPORTED
Implicit Arguments infima [X].
@@ -220,9 +220,9 @@ A non-empty totally bounded sub-pseudo-metric-space $P$#P# is said to be
all points that are in some sense close to $P$#P#.
*)
-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
*)