# Sections of a multiset #

def Multiset.Sections {α : Type u_1} (s : 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 a member of the corresponding multiset.

Equations
• s.Sections = s.recOn {0} (fun (s : ) (x c : Multiset ()) => s.bind fun (a : α) => )
Instances For
@[simp]
theorem Multiset.sections_zero {α : Type u_1} :
= {0}
@[simp]
theorem Multiset.sections_cons {α : Type u_1} (s : Multiset ()) (m : ) :
(m ::ₘ s).Sections = m.bind fun (a : α) => Multiset.map () s.Sections
theorem Multiset.coe_sections {α : Type u_1} (l : List (List α)) :
((List.map (fun (l : List α) => l) l)).Sections = (List.map (fun (l : List α) => l) l.sections)
@[simp]
theorem Multiset.sections_add {α : Type u_1} (s : Multiset ()) (t : Multiset ()) :
(s + t).Sections = s.Sections.bind fun (m : ) => Multiset.map (fun (x : ) => m + x) t.Sections
theorem Multiset.mem_sections {α : Type u_1} {s : Multiset ()} {a : } :
a s.Sections Multiset.Rel (fun (s : ) (a : α) => a s) s a
theorem Multiset.card_sections {α : Type u_1} {s : Multiset ()} :
Multiset.card s.Sections = (Multiset.map (Multiset.card) s).prod
theorem Multiset.prod_map_sum {α : Type u_1} [] {s : Multiset ()} :
(Multiset.map Multiset.sum s).prod = (Multiset.map Multiset.prod s.Sections).sum