Nuprl Definition : sub-powerset-lattice
sub-powerset-lattice(T;eq;whole;P) == {points={s:fset(T)| P s} ;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),
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
set: {x:A| B[x]} ,
fset: fset(T),
apply: f a,
fset-intersection: a ⋂ b,
lambda: λx.A[x],
fset-union: x ⋃ y,
empty-fset: {}
FDL editor aliases :
sub-powerset-lattice
Latex:
sub-powerset-lattice(T;eq;whole;P) == \{points=\{s:fset(T)| P s\} ;meet=\mlambda{}a,b. a \mcap{} b;join=\mlambda{}a,b. a \mcup{} b;0\000C=\{\};1=whole\}
Date html generated:
2020_05_20-AM-08_47_34
Last ObjectModification:
2015_10_06-PM-01_44_04
Theory : lattices
Home
Index