### 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: 2016_05_18-AM-11_21_21
Last ObjectModification: 2015_10_06-PM-01_45_28

Theory : lattices

Home Index