Multiset.sections_cons

theorem Multiset.sections_cons : ∀ {α : Type u_1} (s : Multiset (Multiset α)) (m : Multiset α), (m ::ₘ s).Sections = m.bind fun a => Multiset.map (Multiset.cons a) s.Sections

The theorem `Multiset.sections_cons` states that for any type `α`, and for any multisets `s` of multisets of `α` and `m` of `α`, the sections of the multiset formed by prepending `m` to `s` is equal to the multiset obtained by binding `m` with a function that maps each element `a` of `m` to the multiset obtained by prepending `a` to each element of the sections of `s`. In other words, it tells us how the sections operation behaves when a new multiset is added to the front of a multiset of multisets.

More concisely: For any type `α` and multisets `s` of multisets and `m` of elements of `α`, the sections of the multiset formed by prepending `m` to `s` is equal to the multiset obtained by binding `m` to a function that maps each element to the multiset obtained by prepending that element to each element of the sections of `s` (i.e., `Multiset.sections (multiset.cons s m) = multiset.bind m (λ a, Multiset.sections (multiset.map (λ s, multiset.cons s a) (Multiset.sections s)))`).