Nuprl Definition : oal_umap
umap(h,f) == λps:|oal(s;g)|. msFor{h} k ∈ dom(ps). (f k (ps[k]))
Definitions occuring in Statement :
lookup: as[k],
oal_dom: dom(ps),
oalist: oal(a;b),
mset_for: mset_for,
tlambda: λx:T. b[x],
apply: f a,
grp_id: e,
set_car: |p|
Definitions occuring in definition :
tlambda: λx:T. b[x],
set_car: |p|,
oalist: oal(a;b),
mset_for: mset_for,
oal_dom: dom(ps),
apply: f a,
lookup: as[k],
grp_id: e
Latex:
umap(h,f) == \mlambda{}ps:|oal(s;g)|. msFor\{h\} k \mmember{} dom(ps). (f k (ps[k]))
Date html generated:
2016_05_16-AM-08_22_54
Last ObjectModification:
2015_09_23-AM-09_53_09
Theory : polynom_2
Home
Index