Nuprl Definition : bag-eq
bag-eq(eq;as;bs) == bag-all(x.((#x in as) =z (#x in bs));as) ∧b bag-all(x.0 <z (#x in as);bs)
Definitions occuring in Statement :
bag-count: (#x in bs),
bag-all: bag-all(x.p[x];bs),
band: p ∧b q,
lt_int: i <z j,
eq_int: (i =z j),
natural_number: $n
Definitions occuring in definition :
band: p ∧b q,
eq_int: (i =z j),
bag-all: bag-all(x.p[x];bs),
lt_int: i <z j,
natural_number: $n,
bag-count: (#x in bs)
FDL editor aliases :
bag-eq
Latex:
bag-eq(eq;as;bs) == bag-all(x.((\#x in as) =\msubz{} (\#x in bs));as) \mwedge{}\msubb{} bag-all(x.0 <z (\#x in as);bs)
Date html generated:
2016_05_15-PM-08_00_20
Last ObjectModification:
2015_09_23-AM-08_20_42
Theory : bags_2
Home
Index