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