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: 2016_05_18-AM-11_28_47
Last ObjectModification: 2015_10_06-PM-01_43_56

Theory : lattices


Home Index