Nuprl Definition : finite-powerset-lattice
finite-powerset-lattice(T;eq;whole) == {points=fset(T);meet=λa,b. a ⋂ b;join=λa,b. a ⋃ b;0={};1=whole}
Definitions occuring in Statement :
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
empty-fset: {},
fset-intersection: a ⋂ b,
fset-union: x ⋃ y,
fset: fset(T),
lambda: λx.A[x]
Definitions occuring in definition :
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
fset: fset(T),
fset-intersection: a ⋂ b,
lambda: λx.A[x],
fset-union: x ⋃ y,
empty-fset: {}
FDL editor aliases :
finite-powerset-lattice
Latex:
finite-powerset-lattice(T;eq;whole) == \{points=fset(T);meet=\mlambda{}a,b. a \mcap{} b;join=\mlambda{}a,b. a \mcup{} b;0=\{\};1=who\000Cle\}
Date html generated:
2020_05_20-AM-08_47_28
Last ObjectModification:
2015_10_06-PM-01_44_07
Theory : lattices
Home
Index