helm/software/matita/contribs/procedural/CoRN/metrics/CPseudoMSpaces.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: CPseudoMSpaces.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *)
  20
  21 include "reals/Intervals.ma".
  22
  23 (*#* *Metric Spaces
  24 *)
  25
  26 (* UNEXPORTED
  27 Section Relations
  28 *)
  29
  30 (*#* **Relations necessary for Pseudo Metric Spaces and Metric Spaces
  31 %\begin{convention}%
  32 Let [A : CSetoid], [d : (CSetoid_bin_fun A A IR)].
  33 %\end{convention}%
  34 *)
  35
  36 (* UNEXPORTED
  37 cic:/CoRN/metrics/CPseudoMSpaces/Relations/A.var
  38 *)
  39
  40 (* UNEXPORTED
  41 cic:/CoRN/metrics/CPseudoMSpaces/Relations/d.var
  42 *)
  43
  44 (* UNEXPORTED
  45 Set Implicit Arguments.
  46 *)
  47
  48 (* UNEXPORTED
  49 Unset Strict Implicit.
  50 *)
  51
  52 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/com.con" as definition.
  53
  54 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/nneg.con" as definition.
  55
  56 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/pos_imp_ap.con" as definition.
  57
  58 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/tri_ineq.con" as definition.
  59
  60 (* UNEXPORTED
  61 Set Strict Implicit.
  62 *)
  63
  64 (* UNEXPORTED
  65 Unset Implicit Arguments.
  66 *)
  67
  68 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/diag_zero.con" as definition.
  69
  70 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/apdiag_imp_grzero.con" as definition.
  71
  72 (* UNEXPORTED
  73 End Relations
  74 *)
  75
  76 (* UNEXPORTED
  77 Section Definition_PsMS0
  78 *)
  79
  80 (*#* **Definition of Pseudo Metric Space
  81 *)
  82
  83 (*#*
  84 A pseudo metric space consists of a setoid and a %''pseudo metric''% #"pseudo metric"#, also called
  85 %''distance''% #"distance"#, a binairy function that fulfils certain properties.
  86 *)
  87
  88 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/is_CPsMetricSpace.ind".
  89
  90 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/CPsMetricSpace.ind".
  91
  92 (* COERCION
  93 cic:/matita/CoRN-Procedural/metrics/CPseudoMSpaces/cms_crr.con
  94 *)
  95
  96 (* UNEXPORTED
  97 End Definition_PsMS0
  98 *)
  99
 100 (* UNEXPORTED
 101 Implicit Arguments cms_d [c].
 102 *)
 103
 104 (* NOTATION
 105 Infix "[-d]" := cms_d (at level 68, left associativity).
 106 *)
 107
 108 (* UNEXPORTED
 109 Section PsMS_axioms
 110 *)
 111
 112 (*#* **Pseudo Metric Space axioms
 113 %\begin{convention}%
 114 Let [A] be a pseudo metric space.
 115 %\end{convention}%
 116 *)
 117
 118 (* UNEXPORTED
 119 cic:/CoRN/metrics/CPseudoMSpaces/PsMS_axioms/A.var
 120 *)
 121
 122 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/CPsMetricSpace_is_CPsMetricSpace.con" as lemma.
 123
 124 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/d_com.con" as lemma.
 125
 126 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/d_nneg.con" as lemma.
 127
 128 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/d_pos_imp_ap.con" as lemma.
 129
 130 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/d_tri_ineq.con" as lemma.
 131
 132 (* UNEXPORTED
 133 End PsMS_axioms
 134 *)
 135
 136 (* UNEXPORTED
 137 Section PsMS_basics
 138 *)
 139
 140 (*#* **Pseudo Metric Space basics
 141 %\begin{convention}%
 142 Let [Y] be a pseudo metric space.
 143 %\end{convention}%
 144 *)
 145
 146 (* UNEXPORTED
 147 cic:/CoRN/metrics/CPseudoMSpaces/PsMS_basics/Y.var
 148 *)
 149
 150 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/rev_tri_ineq.con" as lemma.
 151
 152 (*#*
 153 Instead of taking [pos_imp_ap] as axiom,
 154 we could as well have taken [diag_zero].
 155 *)
 156
 157 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/diag_zero_imp_pos_imp_ap.con" as lemma.
 158
 159 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/pos_imp_ap_imp_diag_zero.con" as lemma.
 160
 161 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/is_CPsMetricSpace_diag_zero.con" as lemma.
 162
 163 (* UNEXPORTED
 164 End PsMS_basics
 165 *)
 166
 167 (* UNEXPORTED
 168 Section Zerof
 169 *)
 170
 171 (*#* **Zero function
 172 *)
 173
 174 (*#*
 175 Every setoid forms with the binary function that always returns zero,
 176 a pseudo metric space.
 177 *)
 178
 179 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun.con" as definition.
 180
 181 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun_strext.con" as lemma.
 182
 183 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/Zero_fun.con" as definition.
 184
 185 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun_com.con" as lemma.
 186
 187 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun_nneg.con" as lemma.
 188
 189 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun_pos_imp_ap.con" as lemma.
 190
 191 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/zero_fun_tri_ineq.con" as lemma.
 192
 193 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/zf_is_CPsMetricSpace.con" as definition.
 194
 195 inline procedural "cic:/CoRN/metrics/CPseudoMSpaces/zf_as_CPsMetricSpace.con" as definition.
 196
 197 (* UNEXPORTED
 198 End Zerof
 199 *)
 200