Nuprl Definition : fset_of_mset
fset_of_mset(s;a) == msFor{<MSet{s},⋃,0>} x ∈ a. mset_inj{s}(x)
Definitions occuring in Statement :
mset_union_mon: <MSet{s},⋃,0>,
mset_for: mset_for,
mset_inj: mset_inj{s}(x)
Definitions occuring in definition :
mset_for: mset_for,
mset_union_mon: <MSet{s},⋃,0>,
mset_inj: mset_inj{s}(x)
Latex:
fset\_of\_mset(s;a) == msFor\{<MSet\{s\},\mcup{},0>\} x \mmember{} a. mset\_inj\{s\}(x)
Date html generated:
2016_05_16-AM-07_50_10
Last ObjectModification:
2015_09_23-AM-09_52_16
Theory : mset
Home
Index