...

[helm.git] / helm / software / matita / dama / metric_lattice.ma

diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index 9f5811b6d710c0c896f3b74c04bb8d29ab757fa1..fdd49fe57355f541983ef5084393a72fea2d2db6 100644 (file)
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -39,6 +39,11 @@ record mlattice (R : todgroup) : Type ≝ {
   ml_prop2: ∀a,b,c:ml_carr. δ (a∨b) (a∨c) + δ (a∧b) (a∧c) ≤ (δ b c)
 }.
 
+interpretation "Metric lattice leq" 'leq a b = 
+  (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice1.con _ _) a b). 
+interpretation "Metric lattice geq" 'geq a b = 
+  (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice.con _ _) a b). 
+
 lemma eq_to_ndlt0: ∀R.∀ml:mlattice R.∀a,b:ml. a ≈ b → ¬ 0 < δ a b.
 intros (R ml a b E); intro H; apply E; apply ml_prop1;
 assumption;