Nuprl Definition : quotient-dl
l//x,y.eq[x; y] ==  {points=x,y:Point(l)//eq[x; y];meet=l."meet";join=l."join";0=l."0";1=l."1"}
Definitions occuring in Statement : 
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice, 
lattice-point: Point(l)
, 
record-select: r.x
, 
quotient: x,y:A//B[x; y]
, 
token: "$token"
Definitions occuring in definition : 
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice, 
quotient: x,y:A//B[x; y]
, 
lattice-point: Point(l)
, 
record-select: r.x
, 
token: "$token"
FDL editor aliases : 
quotient-dl
Latex:
l//x,y.eq[x;  y]  ==    \{points=x,y:Point(l)//eq[x;  y];meet=l."meet";join=l."join";0=l."0";1=l."1"\}
Date html generated:
2020_05_20-AM-08_58_45
Last ObjectModification:
2017_01_23-PM-05_27_44
Theory : lattices
Home
Index