mathlib3 documentation


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.

theorem multiset.sections_zero {α : Type u_1} :
0.sections = {0}
theorem multiset.sections_cons {α : Type u_1} (s : multiset (multiset α)) (m : multiset α) :
(m ::ₘ s).sections = m.bind (λ (a : α), (multiset.cons a) s.sections)
theorem multiset.coe_sections {α : Type u_1} (l : list (list α)) :
( (λ (l : list α), l) l).sections = ( (λ (l : list α), l) l.sections)
theorem multiset.sections_add {α : Type u_1} (s t : multiset (multiset α)) :
theorem multiset.mem_sections {α : Type u_1} {s : multiset (multiset α)} {a : multiset α} :
a s.sections multiset.rel (λ (s : multiset α) (a : α), a s) s a