helm/software/matita/dama/metric_set.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 set "baseuri" "cic:/matita/metric_set/".
  16
  17 include "ordered_groups.ma".
  18
  19 record metric_set (R : ogroup) : Type ≝ {
  20   ms_carr :> Type;
  21   metric: ms_carr → ms_carr → R;
  22   mpositive: ∀a,b:ms_carr. metric a b ≤ 0;
  23   mreflexive: ∀a. metric a a ≈ 0;
  24   msymmetric: ∀a,b. metric a b ≈ metric b a;
  25   mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b
  26   (* manca qualcosa per essere una metrica e non una semimetrica *)
  27 }.
  28
  29 notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
  30 interpretation "metric" 'delta2 a b = (cic:/matita/metric_set/metric.con _ _ a b).
  31 notation "\delta" non associative with precedence 80 for @{ 'delta }.
  32 interpretation "metric" 'delta = (cic:/matita/metric_set/metric.con _ _).