matita/contribs/CoRN-Decl/metrics/CMetricSpaces.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/CMetricSpaces".
  18
  19 (* $Id: CMetricSpaces.v,v 1.4 2004/04/23 10:01:01 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 Prod_Sub
  23 *)
  24
  25 (* INCLUDE
  26 Equiv
  27 *)
  28
  29 (* UNEXPORTED
  30 Section Definition_MS.
  31 *)
  32
  33 (*#* **Definition of Metric Space
  34 *)
  35
  36 inline cic:/CoRN/metrics/CMetricSpaces/CMetricSpace.ind.
  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 cic:/CoRN/metrics/CMetricSpaces/d_CMetricSpace_apdiag_imp_grzero.con.
  50
  51 inline cic:/CoRN/metrics/CMetricSpaces/d_zero_imp_eq.con.
  52
  53 inline cic:/CoRN/metrics/CMetricSpaces/is_CMetricSpace_diag_zero.con.
  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 cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpaces_apdiag_grzero.con.
  71
  72 inline cic:/CoRN/metrics/CMetricSpaces/Prod0CMetricSpace.con.
  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 cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace_apdiag_grzero.con.
  83
  84 inline cic:/CoRN/metrics/CMetricSpaces/SubMetricSpace.con.
  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 cic:/CoRN/metrics/CMetricSpaces/zf_nis_CMetricSpace.con.
 106
 107 (*#*
 108 But a pseudo metric space induces a metric space:
 109 *)
 110
 111 inline cic:/CoRN/metrics/CMetricSpaces/metric_ap.con.
 112
 113 inline cic:/CoRN/metrics/CMetricSpaces/metric_eq.con.
 114
 115 inline cic:/CoRN/metrics/CMetricSpaces/metric_ap_irreflexive.con.
 116
 117 inline cic:/CoRN/metrics/CMetricSpaces/metric_ap_symmetric.con.
 118
 119 inline cic:/CoRN/metrics/CMetricSpaces/metric_ap_cotransitive.con.
 120
 121 inline cic:/CoRN/metrics/CMetricSpaces/metric_ap_tight.con.
 122
 123 inline cic:/CoRN/metrics/CMetricSpaces/Metric_CSet_is_CSetoid.con.
 124
 125 inline cic:/CoRN/metrics/CMetricSpaces/Metric_CSetoid.con.
 126
 127 inline cic:/CoRN/metrics/CMetricSpaces/metric_d.con.
 128
 129 inline cic:/CoRN/metrics/CMetricSpaces/metric_d_strext.con.
 130
 131 inline cic:/CoRN/metrics/CMetricSpaces/Metric_d.con.
 132
 133 inline cic:/CoRN/metrics/CMetricSpaces/Metric_d_com.con.
 134
 135 inline cic:/CoRN/metrics/CMetricSpaces/Metric_d_nneg.con.
 136
 137 inline cic:/CoRN/metrics/CMetricSpaces/Metric_d_pos_imp_ap.con.
 138
 139 inline cic:/CoRN/metrics/CMetricSpaces/Metric_d_tri_ineq.con.
 140
 141 inline cic:/CoRN/metrics/CMetricSpaces/QuotientCSetoid_is_CPsMetricSpace.con.
 142
 143 inline cic:/CoRN/metrics/CMetricSpaces/QuotientCPsMetricSpace.con.
 144
 145 inline cic:/CoRN/metrics/CMetricSpaces/Metric_d_apdiag_grzero.con.
 146
 147 inline cic:/CoRN/metrics/CMetricSpaces/QuotientCMetricSpace.con.
 148
 149 (*#*
 150 Some pseudo metric spaces already are a metric space:
 151 *)
 152
 153 inline cic:/CoRN/metrics/CMetricSpaces/dIR_apdiag_grzero.con.
 154
 155 inline cic:/CoRN/metrics/CMetricSpaces/IR_as_CMetricSpace.con.
 156
 157 (*#*
 158 In that case the induced metric space is equivalent to the original one:
 159 *)
 160
 161 inline cic:/CoRN/metrics/CMetricSpaces/emb.con.
 162
 163 inline cic:/CoRN/metrics/CMetricSpaces/emb_strext.con.
 164
 165 inline cic:/CoRN/metrics/CMetricSpaces/Emb.con.
 166
 167 inline cic:/CoRN/metrics/CMetricSpaces/Quotient_pres_CMetricSpace.con.
 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 cic:/CoRN/metrics/CMetricSpaces/nz.con.
 191
 192 (* end hide *)
 193
 194 (* begin hide *)
 195
 196 inline cic:/CoRN/metrics/CMetricSpaces/d_wd.con.
 197
 198 (* end hide *)
 199
 200 inline cic:/CoRN/metrics/CMetricSpaces/unique_MSseqLim.con.
 201
 202 (* UNEXPORTED
 203 End Limitt.
 204 *)
 205