...

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

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 398b1af89dc0c6c69f7e7dbc3203a0b47773483d..20d746a0a69ca9a5517e04bb2de3a5012d94713c 100644 (file)
--- 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 =