Nuprl Definition : general-bounded-lattice-structure
A generalized bounded lattice structure includes
all the components of a bounded lattice, and, in addition,
a relation E on the points of the lattice.
When we define a generalized bounded lattice, E will be an
equivalence relation on the points, and the lattice axioms
will hold upto E-equivalence.⋅
GeneralBoundedLatticeStructure ==
"Point":Type
"meet":self."Point" ⟶ self."Point" ⟶ self."Point"
"join":self."Point" ⟶ self."Point" ⟶ self."Point"
"1":self."Point"
"0":self."Point"
"E":self."Point" ⟶ self."Point" ⟶ ℙ
Definitions occuring in Statement :
record-select: r.x,
record+: record+,
record: record(x.T[x]),
top: Top,
prop: ℙ,
function: x:A ⟶ B[x],
token: "$token",
universe: Type
Definitions occuring in definition :
record+: record+,
record: record(x.T[x]),
top: Top,
universe: Type,
function: x:A ⟶ B[x],
record-select: r.x,
token: "$token",
prop: ℙ
FDL editor aliases :
general-bounded-lattice-structure
Latex:
GeneralBoundedLatticeStructure ==
"Point":Type
"meet":self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} self."Point"
"join":self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} self."Point"
"1":self."Point"
"0":self."Point"
"E":self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} \mBbbP{}
Date html generated:
2020_05_20-AM-08_57_40
Last ObjectModification:
2016_01_13-PM-04_00_53
Theory : lattices
Home
Index