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.

Instances For
    @[simp]
    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)