Nuprl Definition : distributive-lattice
DistributiveLattice ==
{l:LatticeStructure| lattice-axioms(l) ∧ (∀[a,b,c:Point(l)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l)))}
Definitions occuring in Statement :
lattice-axioms: lattice-axioms(l),
lattice-join: a ∨ b,
lattice-meet: a ∧ b,
lattice-point: Point(l),
lattice-structure: LatticeStructure,
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]} ,
lattice-structure: LatticeStructure,
and: P ∧ Q,
lattice-axioms: 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 :
distributive-lattice
Latex:
DistributiveLattice ==
\{l:LatticeStructure| 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_24_58
Last ObjectModification:
2015_10_06-PM-01_45_33
Theory : lattices
Home
Index