- (cic:/matita/lattices/join.con _ _ a b).
-
-record is_lattice (C:Type) (L:pre_lattice C) : Prop \def
- { (* abelian semigroup properties *)
- l_comm_j: symmetric ? (join ? L);
- l_associative_j: associative ? (join ? L);
- l_comm_m: symmetric ? (meet ? L);
- l_associative_m: associative ? (meet ? L);
- (* other properties *)
- l_adsorb_j_m: ∀f,g:L. (f ∨ f ∧ g) = f;
- l_adsorb_m_j: ∀f,g:L. (f ∧ (f ∨ g)) = f
- }.
-
-record lattice (C:Type) : Type \def
- { l_pre_lattice:> pre_lattice C;
- l_lattice_properties:> is_lattice ? l_pre_lattice
- }.