Nuprl Definition : mset_prod
a × b == msFor{<MSet{g↓set},⋃,0>} u ∈ a. msFor{<MSet{g↓set},⋃,0>} v ∈ b. mset_inj{g↓set}(u * v)
Definitions occuring in Statement :
mset_union_mon: <MSet{s},⋃,0>,
mset_for: mset_for,
mset_inj: mset_inj{s}(x),
infix_ap: x f y,
dset_of_mon: g↓set,
grp_op: *
Definitions occuring in definition :
mset_for: mset_for,
mset_union_mon: <MSet{s},⋃,0>,
mset_inj: mset_inj{s}(x),
dset_of_mon: g↓set,
infix_ap: x f y,
grp_op: *
Latex:
a \mtimes{} b == msFor\{<MSet\{g\mdownarrow{}set\},\mcup{},0>\} u \mmember{} a. msFor\{<MSet\{g\mdownarrow{}set\},\mcup{},0>\} v \mmember{} b. mset\_inj\{g\mdownarrow{}set\}(u * v)
Date html generated:
2016_05_16-AM-07_51_59
Last ObjectModification:
2015_09_23-AM-09_52_22
Theory : mset
Home
Index