Nuprl Definition : mset_map
msmap{s,s'}(f;a) == msFor{mset_mon{s'}} x ∈ a. mset_inj{s'}(f x)
Definitions occuring in Statement :
mset_for: mset_for,
mset_mon: mset_mon{s},
mset_inj: mset_inj{s}(x),
apply: f a
Definitions occuring in definition :
mset_for: mset_for,
mset_mon: mset_mon{s},
mset_inj: mset_inj{s}(x),
apply: f a
Latex:
msmap\{s,s'\}(f;a) == msFor\{mset\_mon\{s'\}\} x \mmember{} a. mset\_inj\{s'\}(f x)
Date html generated:
2016_05_16-AM-07_48_40
Last ObjectModification:
2015_09_23-AM-09_52_11
Theory : mset
Home
Index