Sections of a multiset #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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.