matita/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 include "CoRN.ma".
  20
  21 (* $Id: CMetricSpaces.v,v 1.4 2004/04/23 10:01:01 lcf Exp $ *)
  22
  23 include "metrics/Prod_Sub.ma".
  24
  25 include "metrics/Equiv.ma".
  26
  27 (* UNEXPORTED
  28 Section Definition_MS
  29 *)
  30
  31 (*#* **Definition of Metric Space
  32 *)
  33
  34 inline "cic:/CoRN/metrics/CMetricSpaces/CMetricSpace.ind".
  35
  36 coercion cic:/matita/CoRN-Decl/metrics/CMetricSpaces/scms_crr.con 0 (* compounds *).
  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