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