Nuprl Definition : bag-has-no-repeats
bag-has-no-repeats(eq;b) == (#(bag-remove-repeats(eq;b)) =z #(b))
Definitions occuring in Statement :
bag-remove-repeats: bag-remove-repeats(eq;bs),
bag-size: #(bs),
eq_int: (i =z j)
Definitions occuring in definition :
eq_int: (i =z j),
bag-remove-repeats: bag-remove-repeats(eq;bs),
bag-size: #(bs)
FDL editor aliases :
bag-has-no-repeats
Latex:
bag-has-no-repeats(eq;b) == (\#(bag-remove-repeats(eq;b)) =\msubz{} \#(b))
Date html generated:
2016_05_15-PM-08_08_54
Last ObjectModification:
2015_09_23-AM-08_20_56
Theory : bags_2
Home
Index