Nuprl Definition : general-bounded-distributive-lattice
GeneralBoundedDistributiveLattice ==
{l:GeneralBoundedLatticeStructure| general-lattice-axioms(l) ∧ (∀[a,b,c:Point(l)]. a ∧ b ∨ c ≡ a ∧ b ∨ a ∧ c)}
Definitions occuring in Statement :
general-lattice-axioms: general-lattice-axioms(l),
lattice-equiv: a ≡ b,
general-bounded-lattice-structure: GeneralBoundedLatticeStructure,
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]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
general-bounded-lattice-structure: GeneralBoundedLatticeStructure,
and: P ∧ Q,
general-lattice-axioms: general-lattice-axioms(l),
uall: ∀[x:A]. B[x],
lattice-point: Point(l),
lattice-equiv: a ≡ b,
lattice-join: a ∨ b,
lattice-meet: a ∧ b
FDL editor aliases :
general-bounded-distributive-lattice
Latex:
GeneralBoundedDistributiveLattice ==
\{l:GeneralBoundedLatticeStructure|
general-lattice-axioms(l) \mwedge{} (\mforall{}[a,b,c:Point(l)]. a \mwedge{} b \mvee{} c \mequiv{} a \mwedge{} b \mvee{} a \mwedge{} c)\}
Date html generated:
2020_05_20-AM-08_58_28
Last ObjectModification:
2015_10_16-PM-04_20_14
Theory : lattices
Home
Index