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

• Multiset.Sections s = Multiset.recOn s {0} (fun (s : Multiset α) (x c : Multiset (Multiset α)) => Multiset.bind s 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 α) : Multiset.Sections (m ::ₘ s) = Multiset.bind m fun (a : α) => Multiset.map (Multiset.cons a) (Multiset.Sections s)

theorem Multiset.coe_sections {α : Type u_1} (l : List (List α)) : Multiset.Sections ↑(List.map (fun (l : List α) => ↑l) l) = ↑(List.map (fun (l : List α) => ↑l) (List.sections l))

@[simp]

theorem Multiset.sections_add {α : Type u_1} (s : Multiset (Multiset α)) (t : Multiset (Multiset α)) : Multiset.Sections (s + t) = Multiset.bind (Multiset.Sections s) fun (m : Multiset α) => Multiset.map (fun (x : Multiset α) => m + x) (Multiset.Sections t)

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

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

theorem Multiset.prod_map_sum {α : Type u_1} [CommSemiring α] {s : Multiset (Multiset α)} : Multiset.prod (Multiset.map Multiset.sum s) = Multiset.sum (Multiset.map Multiset.prod (Multiset.Sections s))