Sections of a multiset #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

s.sections = s.rec_on {0} (λ (s : multiset α) (_x c : multiset (multiset α)), s.bind (λ (a : α), multiset.map (multiset.cons a) c)) multiset.sections._proof_1

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