helm/software/matita/contribs/procedural/CoRN/metrics/CMetricSpaces.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: CMetricSpaces.v,v 1.4 2004/04/23 10:01:01 lcf Exp $ *)
  20
  21 include "metrics/Prod_Sub.ma".
  22
  23 include "metrics/Equiv.ma".
  24
  25 (* UNEXPORTED
  26 Section Definition_MS
  27 *)
  28
  29 (*#* **Definition of Metric Space
  30 *)
  31
  32 inline procedural "cic:/CoRN/metrics/CMetricSpaces/CMetricSpace.ind".
  33
  34 (* COERCION
  35 cic:/matita/CoRN-Procedural/metrics/CMetricSpaces/scms_crr.con
  36 *)
  37
  38 (* UNEXPORTED
  39 End Definition_MS
  40 *)
  41
  42 (* UNEXPORTED
  43 Section MS_basics
  44 *)
  45
  46 (*#* **Metric Space basics
  47 *)
  48
  49 inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_CMetricSpace_apdiag_imp_grzero.con" as lemma.
  50
  51 inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con" as lemma.
  52
  53 inline procedural "cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con" as lemma.
  54
  55 (* UNEXPORTED
  56 End MS_basics
  57 *)
  58
  59 (* UNEXPORTED
  60 Section prodandsub
  61 *)
  62
  63 (*#* **Product-Metric-Spaces and Sub-Metric-Spaces
  64 *)
  65
  66 (*#*
  67 The product of two metric spaces is again a metric space.
  68 *)
  69
  70 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpaces_apdiag_grzero.con" as lemma.
  71
  72 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpace.con" as definition.
  73
  74 (*#*
  75 A subspace of a metric space is again a metric space.
  76 *)
  77
  78 (* UNEXPORTED
  79 Implicit Arguments SubPsMetricSpace [X].
  80 *)
  81
  82 inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace_apdiag_grzero.con" as lemma.
  83
  84 inline procedural "cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace.con" as definition.
  85
  86 (* UNEXPORTED
  87 Implicit Arguments SubMetricSpace [X].
  88 *)
  89
  90 (* UNEXPORTED
  91 End prodandsub
  92 *)
  93
  94 (* UNEXPORTED
  95 Section Zeroff
  96 *)
  97
  98 (*#* **Pseudo Metric Spaces vs Metric Spaces
  99 *)
 100
 101 (*#*
 102 Not all pseudo metric spaces are a metric space:
 103 *)
 104
 105 inline procedural "cic:/CoRN/metrics/CMetricSpaces/zf_nis_CMetricSpace.con" as lemma.
 106
 107 (*#*
 108 But a pseudo metric space induces a metric space:
 109 *)
 110
 111 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap.con" as definition.
 112
 113 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_eq.con" as definition.
 114
 115 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_irreflexive.con" as lemma.
 116
 117 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_symmetric.con" as lemma.
 118
 119 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_cotransitive.con" as lemma.
 120
 121 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_ap_tight.con" as lemma.
 122
 123 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSet_is_CSetoid.con" as definition.
 124
 125 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_CSetoid.con" as definition.
 126
 127 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d.con" as definition.
 128
 129 inline procedural "cic:/CoRN/metrics/CMetricSpaces/metric_d_strext.con" as lemma.
 130
 131 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d.con" as definition.
 132
 133 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_com.con" as lemma.
 134
 135 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_nneg.con" as lemma.
 136
 137 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_pos_imp_ap.con" as lemma.
 138
 139 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_tri_ineq.con" as lemma.
 140
 141 inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCSetoid_is_CPsMetricSpace.con" as definition.
 142
 143 inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCPsMetricSpace.con" as definition.
 144
 145 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Metric_d_apdiag_grzero.con" as lemma.
 146
 147 inline procedural "cic:/CoRN/metrics/CMetricSpaces/QuotientCMetricSpace.con" as definition.
 148
 149 (*#*
 150 Some pseudo metric spaces already are a metric space:
 151 *)
 152
 153 inline procedural "cic:/CoRN/metrics/CMetricSpaces/dIR_apdiag_grzero.con" as lemma.
 154
 155 inline procedural "cic:/CoRN/metrics/CMetricSpaces/IR_as_CMetricSpace.con" as definition.
 156
 157 (*#*
 158 In that case the induced metric space is equivalent to the original one:
 159 *)
 160
 161 inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb.con" as definition.
 162
 163 inline procedural "cic:/CoRN/metrics/CMetricSpaces/emb_strext.con" as lemma.
 164
 165 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Emb.con" as definition.
 166
 167 inline procedural "cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con" as lemma.
 168
 169 (* UNEXPORTED
 170 End Zeroff
 171 *)
 172
 173 (* UNEXPORTED
 174 Section Limitt
 175 *)
 176
 177 (*#* **Limit
 178 *)
 179
 180 (*#*
 181 A sequence in a metric space has at most one limit.
 182 *)
 183
 184 (* UNEXPORTED
 185 Implicit Arguments MSseqLimit [X].
 186 *)
 187
 188 (* begin hide *)
 189
 190 inline procedural "cic:/CoRN/metrics/CMetricSpaces/nz.con" as lemma.
 191
 192 (* end hide *)
 193
 194 (* begin hide *)
 195
 196 inline procedural "cic:/CoRN/metrics/CMetricSpaces/d_wd.con" as lemma.
 197
 198 (* end hide *)
 199
 200 inline procedural "cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con" as lemma.
 201
 202 (* UNEXPORTED
 203 End Limitt
 204 *)
 205