# mathlibdocumentation

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
@[simp]
theorem multiset.sections_zero {α : Type u_1} :
0.sections = {0}
@[simp]
theorem multiset.sections_cons {α : Type u_1} (s : multiset (multiset α)) (m : multiset α) :
(m ::ₘ s).sections = m.bind (λ (a : α),
theorem multiset.coe_sections {α : Type u_1} (l : list (list α)) :
(list.map (λ (l : list α), l) l).sections = (list.map (λ (l : list α), l) l.sections)
@[simp]
theorem multiset.sections_add {α : Type u_1} (s t : multiset (multiset α)) :
(s + t).sections = s.sections.bind (λ (m : multiset α), t.sections)
theorem multiset.mem_sections {α : Type u_1} {s : multiset (multiset α)} {a : multiset α} :
a s.sections multiset.rel (λ (s : multiset α) (a : α), a s) s a
theorem multiset.card_sections {α : Type u_1} {s : multiset (multiset α)} :
theorem multiset.prod_map_sum {α : Type u_1} {s : multiset (multiset α)} :