Nuprl Definition : list-powerset
list-powerset(eq;L) == reduce(λu,p. p ⋃ λs.fset-add(eq;u;s)"(p);{{}};L)
Definitions occuring in Statement :
fset-image: f"(s),
deq-fset: deq-fset(eq),
empty-fset: {},
fset-add: fset-add(eq;x;s),
fset-singleton: {x},
fset-union: x ⋃ y,
reduce: reduce(f;k;as),
lambda: λx.A[x]
Definitions occuring in definition :
reduce: reduce(f;k;as),
fset-union: x ⋃ y,
fset-image: f"(s),
deq-fset: deq-fset(eq),
lambda: λx.A[x],
fset-add: fset-add(eq;x;s),
fset-singleton: {x},
empty-fset: {}
FDL editor aliases :
list-powerset
Latex:
list-powerset(eq;L) == reduce(\mlambda{}u,p. p \mcup{} \mlambda{}s.fset-add(eq;u;s)"(p);\{\{\}\};L)
Date html generated:
2016_05_14-PM-03_48_13
Last ObjectModification:
2015_10_06-PM-01_33_20
Theory : finite!sets
Home
Index