Nuprl Definition : general-lattice-axioms

E is an equivalence relation on the lattice points.
The usual axioms for a bounded lattice hold "upto E-equivalence".

For example the (constructive) real numbers in a closed interval
form a generalized bounded lattice where E is ⌜x = y⌝ (req).⋅

general-lattice-axioms(l) ==
  EquivRel(Point(l);a,b.a ≡ b)
  ∧ (∀[a,b:Point(l)].  a ∧ b ≡ b ∧ a)
  ∧ (∀[a,b:Point(l)].  a ∨ b ≡ b ∨ a)
  ∧ (∀[a,b,c:Point(l)].  a ∧ b ∧ c ≡ a ∧ b ∧ c)
  ∧ (∀[a,b,c:Point(l)].  a ∨ b ∨ c ≡ a ∨ b ∨ c)
  ∧ (∀[a,b:Point(l)].  a ∨ a ∧ b ≡ a)
  ∧ (∀[a,b:Point(l)].  a ∧ a ∨ b ≡ a)
  ∧ (∀[a:Point(l)]. a ∨ 0 ≡ a)
  ∧ (∀[a:Point(l)]. a ∧ 1 ≡ a)

Definitions occuring in Statement : lattice-equiv: a ≡ b, lattice-0: 0, lattice-1: 1, lattice-join: a ∨ b, lattice-meet: a ∧ b, lattice-point: Point(l), equiv_rel: EquivRel(T;x,y.E[x; y]), uall: ∀[x:A]. B[x], and: P ∧ Q
Definitions occuring in definition : equiv_rel: EquivRel(T;x,y.E[x; y]), and: P ∧ Q, lattice-join: a ∨ b, lattice-0: 0, uall: ∀[x:A]. B[x], lattice-point: Point(l), lattice-equiv: a ≡ b, lattice-meet: a ∧ b, lattice-1: 1
FDL editor aliases : general-lattice-axioms

Latex:
general-lattice-axioms(l) == EquivRel(Point(l);a,b.a \mequiv{} b) \mwedge{} (\mforall{}[a,b:Point(l)]. a \mwedge{} b \mequiv{} b \mwedge{} a) \mwedge{} (\mforall{}[a,b:Point(l)]. a \mvee{} b \mequiv{} b \mvee{} a) \mwedge{} (\mforall{}[a,b,c:Point(l)]. a \mwedge{} b \mwedge{} c \mequiv{} a \mwedge{} b \mwedge{} c) \mwedge{} (\mforall{}[a,b,c:Point(l)]. a \mvee{} b \mvee{} c \mequiv{} a \mvee{} b \mvee{} c) \mwedge{} (\mforall{}[a,b:Point(l)]. a \mvee{} a \mwedge{} b \mequiv{} a) \mwedge{} (\mforall{}[a,b:Point(l)]. a \mwedge{} a \mvee{} b \mequiv{} a) \mwedge{} (\mforall{}[a:Point(l)]. a \mvee{} 0 \mequiv{} a) \mwedge{} (\mforall{}[a:Point(l)]. a \mwedge{} 1 \mequiv{} a) Date html generated: 2020_05_20-AM-08_58_02 Last ObjectModification: 2016_01_13-PM-04_03_53 Theory : lattices Home Index