matita/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/metrics/CPMSTheory".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: CPMSTheory.v,v 1.6 2004/04/23 10:01:02 lcf Exp $ *)
  22
  23 include "metrics/Prod_Sub.ma".
  24
  25 (* UNEXPORTED
  26 Section lists
  27 *)
  28
  29 (*#* **Lists
  30 *)
  31
  32 (*#*
  33  List and membership of lists are used in the definition of
  34 %''totally bounded''% #"totally bounded"#. Note that we use the Leibniz equality in the definition
  35 of [MSmember], and not the setoid equality. So we are really talking about
  36 finite sets of representants, instead of finite subsetoids. This seems to make
  37  the proofs a bit easier.
  38 *)
  39
  40 inline "cic:/CoRN/metrics/CPMSTheory/MSmember.con".
  41
  42 (* UNEXPORTED
  43 Implicit Arguments MSmember [X].
  44 *)
  45
  46 inline "cic:/CoRN/metrics/CPMSTheory/to_IR.con".
  47
  48 inline "cic:/CoRN/metrics/CPMSTheory/from_IR.con".
  49
  50 inline "cic:/CoRN/metrics/CPMSTheory/list_IR.con".
  51
  52 inline "cic:/CoRN/metrics/CPMSTheory/is_P.con".
  53
  54 (*#*
  55 If a real number is element of a list in the above defined sense,
  56 it is an element of the list in the sense of [member],
  57 that uses the setoid equality.
  58 *)
  59
  60 inline "cic:/CoRN/metrics/CPMSTheory/member1.con".
  61
  62 (*#*
  63 The image under a certain mapping of an element of a list $l$ #<I>l</I># is member
  64 of the list of images of elements of $l$ #<I>l</I>#.
  65 *)
  66
  67 inline "cic:/CoRN/metrics/CPMSTheory/map_member.con".
  68
  69 (* UNEXPORTED
  70 End lists
  71 *)
  72
  73 (* UNEXPORTED
  74 Section loc_and_bound
  75 *)
  76
  77 (*#* **Pseudo Metric Space theory
  78 *)
  79
  80 inline "cic:/CoRN/metrics/CPMSTheory/Re_co_do.con".
  81
  82 inline "cic:/CoRN/metrics/CPMSTheory/Re_co_do_strext.con".
  83
  84 inline "cic:/CoRN/metrics/CPMSTheory/re_co_do.con".
  85
  86 inline "cic:/CoRN/metrics/CPMSTheory/re_co_do_well_def.con".
  87
  88 (* UNEXPORTED
  89 Implicit Arguments MSmember [X].
  90 *)
  91
  92 (*#*
  93 Again we see that the image under a certain mapping of an element of a list $l$
  94 #<I>l</I># is member of the list of images of elements of $l$ #<I>l</I>#.
  95 *)
  96
  97 inline "cic:/CoRN/metrics/CPMSTheory/map_member'.con".
  98
  99 inline "cic:/CoRN/metrics/CPMSTheory/bounded.con".
 100
 101 inline "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded.con".
 102
 103 (*#*
 104 Total boundedness is preserved under uniformly continuous mappings.
 105 *)
 106
 107 (* UNEXPORTED
 108 Implicit Arguments SubPsMetricSpace [X].
 109 *)
 110
 111 inline "cic:/CoRN/metrics/CPMSTheory/unicon_resp_totallybounded.con".
 112
 113 inline "cic:/CoRN/metrics/CPMSTheory/MStotallybounded_totallybounded.con".
 114
 115 (*#*
 116 Every image under an uniformly continuous function of an totally bounded
 117 pseudo metric space has an infimum and a supremum.
 118 *)
 119
 120 inline "cic:/CoRN/metrics/CPMSTheory/infimum_exists.con".
 121
 122 inline "cic:/CoRN/metrics/CPMSTheory/supremum_exists.con".
 123
 124 (*#*
 125 A subspace $P$#<I>P</I># of a pseudo metric space $X$#<I>X</I># is said to be located if for all
 126 elements $x$#<I>x</I># of $X$#<I>X</I># there exists an infimum for the distance
 127 between $x$#<I>x</I># and the elements of $P$#<I>P</I>#.
 128 *)
 129
 130 (* UNEXPORTED
 131 Implicit Arguments dsub'_as_cs_fun [X].
 132 *)
 133
 134 inline "cic:/CoRN/metrics/CPMSTheory/located.con".
 135
 136 (* UNEXPORTED
 137 Implicit Arguments located [X].
 138 *)
 139
 140 inline "cic:/CoRN/metrics/CPMSTheory/located'.con".
 141
 142 (* UNEXPORTED
 143 Implicit Arguments located' [X].
 144 *)
 145
 146 inline "cic:/CoRN/metrics/CPMSTheory/located_imp_located'.con".
 147
 148 (*#*
 149 Every totally bounded pseudo metric space is located.
 150 *)
 151
 152 inline "cic:/CoRN/metrics/CPMSTheory/MStotally_bounded_imp_located.con".
 153
 154 (*#*
 155 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>#,
 156 [Floc] chooses for a given natural number $n$#<I>n</I># an $y$#<I>y</I># in $P$#<I>P</I># such that:
 157 $d(x,y)\leq \mbox{inf}\{d(x,p)|p \in P\}+(n+1)^{-1}$
 158 #d(x,y) &le; inf&#x007B;d(x,p)&#x007C; p&#x03F5;P&#x007D; + (n+1)<SUP>-1</SUP>#.
 159 [Flocfun] does (almost) the same, but has a different type. This enables
 160 one to use the latter as an argument of [map].
 161 *)
 162
 163 inline "cic:/CoRN/metrics/CPMSTheory/Floc.con".
 164
 165 inline "cic:/CoRN/metrics/CPMSTheory/Flocfun.con".
 166
 167 (*#*
 168 A located subset $P$#<I>P</I># of a totally bounded pseudo metric space $X$
 169 #<I>X</I># is totally
 170 bounded.
 171 *)
 172
 173 inline "cic:/CoRN/metrics/CPMSTheory/locatedsub_totallybounded_imp_totallyboundedsub.con".
 174
 175 (*#*
 176 Here are some definitions that could come in handy:
 177 *)
 178
 179 inline "cic:/CoRN/metrics/CPMSTheory/MSCauchy_seq.con".
 180
 181 (* UNEXPORTED
 182 Implicit Arguments MSseqLimit' [X].
 183 *)
 184
 185 inline "cic:/CoRN/metrics/CPMSTheory/MSComplete.con".
 186
 187 (*#*
 188 A compact pseudo metric space is a pseudo metric space which is complete and
 189 totally bounded.
 190 *)
 191
 192 inline "cic:/CoRN/metrics/CPMSTheory/MSCompact.con".
 193
 194 (*#*
 195 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
 196 with centre $x$#<I>x</I># that is contained in $P$#<I>P</I>#.
 197 *)
 198
 199 inline "cic:/CoRN/metrics/CPMSTheory/open.con".
 200
 201 (* UNEXPORTED
 202 Implicit Arguments open [X].
 203 *)
 204
 205 (*#*
 206 The operator [infima] gives the infimum for the distance between an
 207 element $x$#<I>x</I># of a located pseudo metric space $X$#<I>X</I># and the elements of a
 208 subspace $P$#<I>P</I># of $X$#<I>X</I>#.
 209 *)
 210
 211 inline "cic:/CoRN/metrics/CPMSTheory/infima.con".
 212
 213 (* UNEXPORTED
 214 Implicit Arguments infima [X].
 215 *)
 216
 217 (*#*
 218 A non-empty totally bounded sub-pseudo-metric-space $P$#<I>P</I># is said to be
 219 %\emph{well contained}% #<I>well contained</I># in an open sub-pseudo-metric-space $Q$#<I>Q</I># if $Q$#<I>Q</I># contains
 220 all points that are in some sense close to $P$#<I>P</I>#.
 221 *)
 222
 223 inline "cic:/CoRN/metrics/CPMSTheory/well_contained.con".
 224
 225 (* UNEXPORTED
 226 End loc_and_bound
 227 *)
 228