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.

@[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 => ↑l) l) = ↑(List.map (fun l => ↑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.map ((fun x x_1 => x + x_1) m) (Multiset.Sections t)

theorem Multiset.mem_sections {α : Type u_1} {s : Multiset (Multiset α)} {a : Multiset α} : a ∈ Multiset.Sections s ↔ Multiset.Rel (fun s 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))