X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;fp=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;h=20d746a0a69ca9a5517e04bb2de3a5012d94713c;hb=a2fe87da00fb5b9a39e9a1c7d796c61d4c7346af;hp=398b1af89dc0c6c69f7e7dbc3203a0b47773483d;hpb=ac94d350073aed443070bea5577b5888ed2dc2db;p=helm.git

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 398b1af89..20d746a0a 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -20,12 +20,16 @@ record lattice : Type ≝ {
   l_carr:> apartness;
   join: l_carr → l_carr → l_carr;
   meet: l_carr → l_carr → l_carr;
+  join_refl: ∀x.join x x ≈ x;
+  meet_refl: ∀x.meet x x ≈ x;  
   join_comm: ∀x,y:l_carr. join x y ≈ join y x;
   meet_comm: ∀x,y:l_carr. meet x y ≈ meet y x;
   join_assoc: ∀x,y,z:l_carr. join x (join y z) ≈ join (join x y) z;
   meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet x y) z;
   absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f;
-  absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f
+  absorbmj: ∀f,g:l_carr. meet f (join f g) ≈ f;
+  strong_extj: ∀x.strong_ext ? (join x);
+  strong_extm: ∀x.strong_ext ? (meet x)
 }.
 
 interpretation "Lattice meet" 'and a b =