Sections of a multiset
The sections of a multiset of multisets s consists of all those multisets
which can be put in bijection with s, so each element is an member of the corresponding multiset.
@[simp]
theorem
multiset.sections_add
{α : Type u_1}
(s t : multiset (multiset α)) :
(s + t).sections = s.sections.bind (λ (m : multiset α), multiset.map (has_add.add m) t.sections)
theorem
multiset.card_sections
{α : Type u_1}
{s : multiset (multiset α)} :
s.sections.card = (multiset.map multiset.card s).prod