Sections of a multiset #
@[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))