X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;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$ #<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].
@@ -94,11 +94,11 @@ Again we see that 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".
 
-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$#<I>P</I># of a pseudo metric space $X$#<I>X</I># is said to be located if for all 
@@ -131,25 +131,25 @@ between $x$#<I>x</I># and the elements of $P$#<I>P</I>#.
 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>#,
@@ -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$#<I>P</I># of a totally bounded pseudo metric space $X$
@@ -170,33 +170,33 @@ 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].
@@ -208,7 +208,7 @@ element $x$#<I>x</I># of a located pseudo metric space $X$#<I>X</I># and the ele
 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].
@@ -220,9 +220,9 @@ A non-empty totally bounded sub-pseudo-metric-space $P$#<I>P</I># is said to be
 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
 *)