matita/matita/contribs/procedural/CoRN/metrics/ContFunctions.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: ContFunctions.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *)
  20
  21 include "metrics/CPseudoMSpaces.ma".
  22
  23 (* UNEXPORTED
  24 Section Continuous_functions
  25 *)
  26
  27 (*#* **Continuous functions, uniformly continuous functions and Lipschitz functions
  28 %\begin{convention}%
  29 Let [A] and [B] be pseudo metric spaces.
  30 %\end{convention}%
  31 *)
  32
  33 (* UNEXPORTED
  34 cic:/CoRN/metrics/ContFunctions/Continuous_functions/A.var
  35 *)
  36
  37 (* UNEXPORTED
  38 cic:/CoRN/metrics/ContFunctions/Continuous_functions/B.var
  39 *)
  40
  41 (*#*
  42 We will look at some notions of continuous functions.
  43 *)
  44
  45 inline procedural "cic:/CoRN/metrics/ContFunctions/continuous.con" as definition.
  46
  47 inline procedural "cic:/CoRN/metrics/ContFunctions/continuous'.con" as definition.
  48
  49 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous.con" as definition.
  50
  51 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous'.con" as definition.
  52
  53 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous''.con" as definition.
  54
  55 inline procedural "cic:/CoRN/metrics/ContFunctions/lipschitz.con" as definition.
  56
  57 inline procedural "cic:/CoRN/metrics/ContFunctions/lipschitz'.con" as definition.
  58
  59 (* UNEXPORTED
  60 End Continuous_functions
  61 *)
  62
  63 (* UNEXPORTED
  64 Implicit Arguments continuous [A B].
  65 *)
  66
  67 (* UNEXPORTED
  68 Implicit Arguments uni_continuous [A B].
  69 *)
  70
  71 (* UNEXPORTED
  72 Implicit Arguments lipschitz [A B].
  73 *)
  74
  75 (* UNEXPORTED
  76 Implicit Arguments continuous' [A B].
  77 *)
  78
  79 (* UNEXPORTED
  80 Implicit Arguments uni_continuous' [A B].
  81 *)
  82
  83 (* UNEXPORTED
  84 Implicit Arguments uni_continuous'' [A B].
  85 *)
  86
  87 (* UNEXPORTED
  88 Implicit Arguments lipschitz' [A B].
  89 *)
  90
  91 (* UNEXPORTED
  92 Section Lemmas
  93 *)
  94
  95 (* begin hide *)
  96
  97 inline procedural "cic:/CoRN/metrics/ContFunctions/nexp_power.con" as lemma.
  98
  99 (* end hide *)
 100
 101 inline procedural "cic:/CoRN/metrics/ContFunctions/continuous_imp_continuous'.con" as lemma.
 102
 103 inline procedural "cic:/CoRN/metrics/ContFunctions/continuous'_imp_continuous.con" as lemma.
 104
 105 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_uni_continuous'.con" as lemma.
 106
 107 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous.con" as lemma.
 108
 109 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous'_imp_uni_continuous''.con" as lemma.
 110
 111 inline procedural "cic:/CoRN/metrics/ContFunctions/lipschitz_imp_lipschitz'.con" as lemma.
 112
 113 inline procedural "cic:/CoRN/metrics/ContFunctions/lipschitz'_imp_lipschitz.con" as lemma.
 114
 115 (*#*
 116 Every uniformly continuous function is continuous and
 117 every Lipschitz function is uniformly continuous.
 118 *)
 119
 120 inline procedural "cic:/CoRN/metrics/ContFunctions/uni_continuous_imp_continuous.con" as lemma.
 121
 122 inline procedural "cic:/CoRN/metrics/ContFunctions/lipschitz_imp_uni_continuous.con" as lemma.
 123
 124 (* UNEXPORTED
 125 End Lemmas
 126 *)
 127
 128 (* UNEXPORTED
 129 Section Identity
 130 *)
 131
 132 (*#* **Identity
 133 *)
 134
 135 (*#*
 136 The identity function is Lipschitz.
 137 Hence it is uniformly continuous and continuous.
 138 *)
 139
 140 inline procedural "cic:/CoRN/metrics/ContFunctions/id_is_lipschitz.con" as lemma.
 141
 142 inline procedural "cic:/CoRN/metrics/ContFunctions/id_is_uni_continuous.con" as lemma.
 143
 144 inline procedural "cic:/CoRN/metrics/ContFunctions/id_is_continuous.con" as lemma.
 145
 146 (* UNEXPORTED
 147 End Identity
 148 *)
 149
 150 (* UNEXPORTED
 151 Section Constant
 152 *)
 153
 154 (*#* **Constant functions
 155 %\begin{convention}%
 156 Let [B] and [X] be pseudo metric spaces.
 157 %\end{convention}%
 158 *)
 159
 160 (*#*
 161 Any constant function is Lipschitz.
 162 Hence it is uniformly continuous and continuous.
 163 *)
 164
 165 (* UNEXPORTED
 166 cic:/CoRN/metrics/ContFunctions/Constant/B.var
 167 *)
 168
 169 (* UNEXPORTED
 170 cic:/CoRN/metrics/ContFunctions/Constant/X.var
 171 *)
 172
 173 inline procedural "cic:/CoRN/metrics/ContFunctions/const_fun_is_lipschitz.con" as lemma.
 174
 175 inline procedural "cic:/CoRN/metrics/ContFunctions/const_fun_is_uni_continuous.con" as lemma.
 176
 177 inline procedural "cic:/CoRN/metrics/ContFunctions/const_fun_is_continuous.con" as lemma.
 178
 179 (* UNEXPORTED
 180 End Constant
 181 *)
 182
 183 (* UNEXPORTED
 184 Section Composition
 185 *)
 186
 187 (*#* **Composition
 188 %\begin{convention}%
 189 Let [B],[C] and [X] be pseudo metric spaces.
 190 Let [f : (CSetoid_fun X B)] and
 191 [g : (CSetoid_fun  B C)].
 192 %\end{convention}%
 193 *)
 194
 195 (*#*
 196 The composition of two Lipschitz/uniformly continous/continuous functions is
 197 again Lipschitz/uniformly continuous/continuous.
 198 *)
 199
 200 (* UNEXPORTED
 201 cic:/CoRN/metrics/ContFunctions/Composition/X.var
 202 *)
 203
 204 (* UNEXPORTED
 205 cic:/CoRN/metrics/ContFunctions/Composition/B.var
 206 *)
 207
 208 (* UNEXPORTED
 209 cic:/CoRN/metrics/ContFunctions/Composition/f.var
 210 *)
 211
 212 (* UNEXPORTED
 213 cic:/CoRN/metrics/ContFunctions/Composition/C.var
 214 *)
 215
 216 (* UNEXPORTED
 217 cic:/CoRN/metrics/ContFunctions/Composition/g.var
 218 *)
 219
 220 inline procedural "cic:/CoRN/metrics/ContFunctions/comp_resp_lipschitz.con" as lemma.
 221
 222 inline procedural "cic:/CoRN/metrics/ContFunctions/comp_resp_uni_continuous.con" as lemma.
 223
 224 inline procedural "cic:/CoRN/metrics/ContFunctions/comp_resp_continuous.con" as lemma.
 225
 226 (* UNEXPORTED
 227 End Composition
 228 *)
 229
 230 (* UNEXPORTED
 231 Section Limit
 232 *)
 233
 234 (*#* **Limit
 235 *)
 236
 237 inline procedural "cic:/CoRN/metrics/ContFunctions/MSseqLimit.con" as definition.
 238
 239 (* UNEXPORTED
 240 Implicit Arguments MSseqLimit [X].
 241 *)
 242
 243 inline procedural "cic:/CoRN/metrics/ContFunctions/MSseqLimit'.con" as definition.
 244
 245 (* UNEXPORTED
 246 Implicit Arguments MSseqLimit' [X].
 247 *)
 248
 249 inline procedural "cic:/CoRN/metrics/ContFunctions/MSseqLimit_imp_MSseqLimit'.con" as lemma.
 250
 251 inline procedural "cic:/CoRN/metrics/ContFunctions/MSseqLimit'_imp_MSseqLimit.con" as lemma.
 252
 253 inline procedural "cic:/CoRN/metrics/ContFunctions/seqcontinuous'.con" as definition.
 254
 255 (* UNEXPORTED
 256 Implicit Arguments seqcontinuous' [A B].
 257 *)
 258
 259 inline procedural "cic:/CoRN/metrics/ContFunctions/continuous'_imp_seqcontinuous'.con" as lemma.
 260
 261 (* UNEXPORTED
 262 End Limit
 263 *)
 264