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 an member of the corresponding multiset.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Multiset.sections_zero {α : Type u_1} :

Multiset.Sections 0 = {0}

source

ink

@[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)

source

ink

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))

source

ink

@[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)

source

ink

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

source

ink

theorem Multiset.card_sections {α : Type u_1} {s : Multiset (Multiset α)} :

↑Multiset.card (Multiset.Sections s) = Multiset.prod (Multiset.map (↑Multiset.card) s)

source

ink

theorem Multiset.prod_map_sum {α : Type u_1} [inst : CommSemiring α] {s : Multiset (Multiset α)} :

Multiset.prod (Multiset.map Multiset.sum s) = Multiset.sum (Multiset.map Multiset.prod (Multiset.Sections s))