Nuprl Definition : free-dist-lattice
free-dist-lattice(T; eq) ==
{points={ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;
meet=λac1,ac2. fset-ac-glb(eq;ac1;ac2);
join=λac1,ac2. fset-ac-lub(eq;ac1;ac2);
0={};
1={{}}}
Definitions occuring in Statement :
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
fset-ac-glb: fset-ac-glb(eq;ac1;ac2),
fset-ac-lub: fset-ac-lub(eq;ac1;ac2),
fset-antichain: fset-antichain(eq;ac),
empty-fset: {},
fset-singleton: {x},
fset: fset(T),
assert: ↑b,
set: {x:A| B[x]} ,
lambda: λx.A[x]
Definitions occuring in definition :
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
set: {x:A| B[x]} ,
fset: fset(T),
assert: ↑b,
fset-antichain: fset-antichain(eq;ac),
fset-ac-glb: fset-ac-glb(eq;ac1;ac2),
lambda: λx.A[x],
fset-ac-lub: fset-ac-lub(eq;ac1;ac2),
fset-singleton: {x},
empty-fset: {}
Latex:
free-dist-lattice(T; eq) ==
\{points=\{ac:fset(fset(T))| \muparrow{}fset-antichain(eq;ac)\} ;
meet=\mlambda{}ac1,ac2. fset-ac-glb(eq;ac1;ac2);
join=\mlambda{}ac1,ac2. fset-ac-lub(eq;ac1;ac2);
0=\{\};
1=\{\{\}\}\}
Date html generated:
2020_05_20-AM-08_44_53
Last ObjectModification:
2015_10_06-PM-01_43_56
Theory : lattices
Home
Index