Sections of a multiset

def Multiset.Sections {α : Type u_1} (s : Multiset (Multiset α)) : Multiset (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 : Multiset α) (x c : Multiset (Multiset α)) => s.bind fun (a : α) => Multiset.map (Multiset.cons a) c) ⋯

@[simp]

theorem Multiset.sections_zero {α : Type u_1} : Multiset.Sections 0 = {0}

@[simp]

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

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 t : Multiset (Multiset α)) : (s + t).Sections = s.Sections.bind fun (m : Multiset α) => Multiset.map (fun (x : Multiset α) => m + x) t.Sections

theorem Multiset.mem_sections {α : Type u_1} {s : Multiset (Multiset α)} {a : Multiset α} : a ∈ s.Sections ↔ Multiset.Rel (fun (s : Multiset α) (a : α) => a ∈ s) s a

theorem Multiset.card_sections {α : Type u_1} {s : Multiset (Multiset α)} : s.Sections.card = (Multiset.map Multiset.card s).prod