Nuprl Definition : bdd-distributive-lattice
BoundedDistributiveLattice ==
{l:BoundedLatticeStructure|
(lattice-axioms(l) ∧ bounded-lattice-axioms(l)) ∧ (∀[a,b,c:Point(l)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l)))}
Definitions occuring in Statement :
bounded-lattice-axioms: bounded-lattice-axioms(l),
bounded-lattice-structure: BoundedLatticeStructure,
lattice-axioms: lattice-axioms(l),
lattice-join: a ∨ b,
lattice-meet: a ∧ b,
lattice-point: Point(l),
uall: ∀[x:A]. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
bounded-lattice-structure: BoundedLatticeStructure,
and: P ∧ Q,
lattice-axioms: lattice-axioms(l),
bounded-lattice-axioms: bounded-lattice-axioms(l),
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
lattice-point: Point(l),
lattice-join: a ∨ b,
lattice-meet: a ∧ b
FDL editor aliases :
bdd-distributive-lattice
Latex:
BoundedDistributiveLattice ==
\{l:BoundedLatticeStructure|
(lattice-axioms(l) \mwedge{} bounded-lattice-axioms(l))
\mwedge{} (\mforall{}[a,b,c:Point(l)]. (a \mwedge{} b \mvee{} c = a \mwedge{} b \mvee{} a \mwedge{} c))\}
Date html generated:
2020_05_20-AM-08_25_04
Last ObjectModification:
2015_10_06-PM-01_45_28
Theory : lattices
Home
Index