mathlib documentation

data.multiset.sections

Sections of a multiset #

source
def multiset.sections {α : Type u_1} (s : multiset (multiset α)) :
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
source
@[simp]
theorem multiset.sections_zero {α : Type u_1} :
0.sections = {0}
source
@[simp]
theorem multiset.sections_cons {α : Type u_1} (s : multiset (multiset α)) (m : multiset α) :
(m ::ₘ s).sections = m.bind (λ (a : α), multiset.map (multiset.cons a) s.sections)
source
theorem multiset.coe_sections {α : Type u_1} (l : list (list α)) :
↑(list.map (λ (l : list α), ↑l) l).sections = ↑(list.map (λ (l : list α), ↑l) l.sections)
source
@[simp]
theorem multiset.sections_add {α : Type u_1} (s t : multiset (multiset α)) :
(s + t).sections = s.sections.bind (λ (m : multiset α), multiset.map (has_add.add m) t.sections)
source
theorem multiset.mem_sections {α : Type u_1} {s : multiset (multiset α)} {a : multiset α} :
a ∈ s.sections ↔ multiset.rel (λ (s : multiset α) (a : α), a ∈ s) s a
source
theorem multiset.card_sections {α : Type u_1} {s : multiset (multiset α)} :
⇑multiset.card s.sections = (multiset.map ⇑multiset.card s).prod
source
theorem multiset.prod_map_sum {α : Type u_1} [comm_semiring α] {s : multiset (multiset α)} :
(multiset.map multiset.sum s).prod = (multiset.map multiset.prod s.sections).sum