Nuprl Definition : mset_inj
mset_inj{s}(x) == mk_mset([x])
Definitions occuring in Statement :
mk_mset: mk_mset(as)
,
cons: [a / b]
,
nil: []
Definitions occuring in definition :
mk_mset: mk_mset(as)
,
cons: [a / b]
,
nil: []
Latex:
mset\_inj\{s\}(x) == mk\_mset([x])
Date html generated:
2016_05_16-AM-07_46_36
Last ObjectModification:
2015_09_23-AM-09_52_02
Theory : mset
Home
Index