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

Equations
  • One or more equations did not get rendered due to their size.
@[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)
theorem Multiset.prod_map_sum {α : Type u_1} [inst : CommSemiring α] {s : Multiset (Multiset α)} :