Nuprl Definition : lattice-axioms
lattice-axioms(l) ==
(∀[a,b:Point(l)]. (a ∧ b = b ∧ a ∈ Point(l)))
∧ (∀[a,b:Point(l)]. (a ∨ b = b ∨ a ∈ Point(l)))
∧ (∀[a,b,c:Point(l)]. (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l)))
∧ (∀[a,b,c:Point(l)]. (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l)))
∧ (∀[a,b:Point(l)]. (a ∨ a ∧ b = a ∈ Point(l)))
∧ (∀[a,b:Point(l)]. (a ∧ a ∨ b = a ∈ Point(l)))
Definitions occuring in Statement :
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,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
lattice-point: Point(l),
lattice-meet: a ∧ b,
lattice-join: a ∨ b
FDL editor aliases :
lattice-axioms
Latex:
lattice-axioms(l) ==
(\mforall{}[a,b:Point(l)]. (a \mwedge{} b = b \mwedge{} a))
\mwedge{} (\mforall{}[a,b:Point(l)]. (a \mvee{} b = b \mvee{} a))
\mwedge{} (\mforall{}[a,b,c:Point(l)]. (a \mwedge{} b \mwedge{} c = a \mwedge{} b \mwedge{} c))
\mwedge{} (\mforall{}[a,b,c:Point(l)]. (a \mvee{} b \mvee{} c = a \mvee{} b \mvee{} c))
\mwedge{} (\mforall{}[a,b:Point(l)]. (a \mvee{} a \mwedge{} b = a))
\mwedge{} (\mforall{}[a,b:Point(l)]. (a \mwedge{} a \mvee{} b = a))
Date html generated:
2020_05_20-AM-08_23_35
Last ObjectModification:
2015_10_06-PM-01_46_03
Theory : lattices
Home
Index