Nuprl Definition : fin-powerset-lattice
fin-powerset-lattice(T;eq) == mk-distributive-lattice(fset(T); λa,b. a ⋂ b; λa,b. a ⋃ b)
Definitions occuring in Statement :
mk-distributive-lattice: mk-distributive-lattice(T; m; j),
fset-intersection: a ⋂ b,
fset-union: x ⋃ y,
fset: fset(T),
lambda: λx.A[x]
Definitions occuring in definition :
mk-distributive-lattice: mk-distributive-lattice(T; m; j),
fset: fset(T),
fset-intersection: a ⋂ b,
lambda: λx.A[x],
fset-union: x ⋃ y
FDL editor aliases :
fin-powerset-lattice
Latex:
fin-powerset-lattice(T;eq) == mk-distributive-lattice(fset(T); \mlambda{}a,b. a \mcap{} b; \mlambda{}a,b. a \mcup{} b)
Date html generated:
2020_05_20-AM-08_47_22
Last ObjectModification:
2015_10_06-PM-01_44_11
Theory : lattices
Home
Index