helm/software/matita/contribs/procedural/CoRN/metrics/CPMSTheory.mma

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