Nuprl Definition : sub-bag

sub-bag(T;as;bs) ==  ∃cs:bag(T). (bs = (as + cs) ∈ bag(T))


Definitions occuring in Statement :  bag-append: as + bs,  bag: bag(T),  exists: ∃x:A. B[x],  equal: s = t ∈ T
Definitions occuring in definition :  exists: ∃x:A. B[x],  equal: s = t ∈ T,  bag: bag(T),  bag-append: as + bs
FDL editor aliases :  sub-bag
Latex:
sub-bag(T;as;bs)  ==    \mexists{}cs:bag(T).  (bs  =  (as  +  cs))


Date html generated: 2016_05_15-PM-02_35_37
Last ObjectModification: 2015_09_23-AM-07_39_51

Theory : bags


Home Index