Nuprl Definition : bag-lub
bag-lub(eq;b1;b2) == ⋃x∈bag-to-set(eq;b1 + b2).bag-rep(imax((#x in b1);(#x in b2));x)
Definitions occuring in Statement :
bag-to-set: bag-to-set(eq;bs),
bag-count: (#x in bs),
bag-rep: bag-rep(n;x),
bag-combine: ⋃x∈bs.f[x],
bag-append: as + bs,
imax: imax(a;b)
Definitions occuring in definition :
bag-combine: ⋃x∈bs.f[x],
bag-to-set: bag-to-set(eq;bs),
bag-append: as + bs,
bag-rep: bag-rep(n;x),
imax: imax(a;b),
bag-count: (#x in bs)
FDL editor aliases :
bag-lub
Latex:
bag-lub(eq;b1;b2) == \mcup{}x\mmember{}bag-to-set(eq;b1 + b2).bag-rep(imax((\#x in b1);(\#x in b2));x)
Date html generated:
2016_05_15-PM-08_09_18
Last ObjectModification:
2015_09_23-AM-08_20_59
Theory : bags_2
Home
Index