Nuprl Definition : omral_alg_umap
alg_umap(n,f) == λps:|omral(g;a)|. Σk ∈ dom(ps). ((ps[k]) n.act (f k))
Definitions occuring in Statement :
omral_dom: dom(ps),
omralist: omral(g;r),
lookup: as[k],
rng_mssum: rng_mssum,
rng_of_alg: a↓rg,
alg_act: a.act,
tlambda: λx:T. b[x],
infix_ap: x f y,
apply: f a,
rng_zero: 0,
oset_of_ocmon: g↓oset,
set_car: |p|
Definitions occuring in definition :
tlambda: λx:T. b[x],
set_car: |p|,
omralist: omral(g;r),
rng_mssum: rng_mssum,
rng_of_alg: a↓rg,
omral_dom: dom(ps),
infix_ap: x f y,
alg_act: a.act,
lookup: as[k],
oset_of_ocmon: g↓oset,
rng_zero: 0,
apply: f a
Latex:
alg\_umap(n,f) == \mlambda{}ps:|omral(g;a)|. \mSigma{}k \mmember{} dom(ps). ((ps[k]) n.act (f k))
Date html generated:
2016_05_16-AM-08_27_35
Last ObjectModification:
2015_09_23-AM-09_53_21
Theory : polynom_3
Home
Index