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