# Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution

Hi.

`Is the subset relation defined in the obvious way for multisets? I.e.
``how do I write
`N is a sub-multiset of M.

`I know that I can define: N is a sub-multiset of M as (ALL b. count N b
``<= count M b)
``but then I will have to prove a host of properties for the sub-multiset
``relation.
`I was wondering if the relation is already defined somewhere?
Thanks,
Revantha.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*