Documentation

Mathlib.Data.Multiset.Sections

Sections of a multiset #

def Multiset.Sections {α : Type u_1} (s : 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
Instances For
    @[simp]
    @[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 : Multiset (Multiset α)) (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 α)} :
    Multiset.card s.Sections = (Multiset.map (Multiset.card) s).prod
    theorem Multiset.prod_map_sum {α : Type u_1} [CommSemiring α] {s : Multiset (Multiset α)} :
    (Multiset.map Multiset.sum s).prod = (Multiset.map Multiset.prod s.Sections).sum