mathlib documentation

data.multiset.basic

Multisets

These are implemented as the quotient of a list by permutations.

Notation

We define the global infix notation ::ₘ for multiset.cons.

def multiset  :
Type uType u

multiset α is the quotient of list α by list permutation. The result is a type of finite sets with duplicates allowed.

Equations
@[instance]
def multiset.has_coe {α : Type u_1} :

Equations
@[simp]
theorem multiset.quot_mk_to_coe {α : Type u_1} (l : list α) :

@[simp]
theorem multiset.quot_mk_to_coe' {α : Type u_1} (l : list α) :
quot.mk has_equiv.equiv l = l

@[simp]
theorem multiset.quot_mk_to_coe'' {α : Type u_1} (l : list α) :
quot.mk setoid.r l = l

@[simp]
theorem multiset.coe_eq_coe {α : Type u_1} {l₁ l₂ : list α} :
l₁ = l₂ l₁ ~ l₂

@[instance]
def multiset.has_decidable_eq {α : Type u_1} [decidable_eq α] :

Equations
def multiset.sizeof {α : Type u_1} [has_sizeof α] :
multiset α

defines a size for a multiset by referring to the size of the underlying list

Equations
@[instance]
def multiset.has_sizeof {α : Type u_1} [has_sizeof α] :

Equations
def multiset.zero {α : Type u_1} :

0 : multiset α is the empty set

Equations
@[instance]
def multiset.has_zero {α : Type u_1} :

Equations
@[instance]
def multiset.has_emptyc {α : Type u_1} :

Equations
@[instance]
def multiset.inhabited {α : Type u_1} :

Equations
@[simp]
theorem multiset.coe_nil_eq_zero {α : Type u_1} :

@[simp]
theorem multiset.empty_eq_zero {α : Type u_1} :
= 0

theorem multiset.coe_eq_zero {α : Type u_1} (l : list α) :

def multiset.cons {α : Type u_1} :
α → multiset αmultiset α

cons a s is the multiset which contains s plus one more instance of a.

Equations
@[instance]
def multiset.has_insert {α : Type u_1} :

Equations
@[simp]
theorem multiset.insert_eq_cons {α : Type u_1} (a : α) (s : multiset α) :
insert a s = a ::ₘ s

@[simp]
theorem multiset.cons_coe {α : Type u_1} (a : α) (l : list α) :
a ::ₘ l = (a :: l)

theorem multiset.singleton_coe {α : Type u_1} (a : α) :
a ::ₘ 0 = [a]

@[simp]
theorem multiset.cons_inj_left {α : Type u_1} {a b : α} (s : multiset α) :
a ::ₘ s = b ::ₘ s a = b

@[simp]
theorem multiset.cons_inj_right {α : Type u_1} (a : α) {s t : multiset α} :
a ::ₘ s = a ::ₘ t s = t

theorem multiset.induction {α : Type u_1} {p : multiset α → Prop} (h₁ : p 0) (h₂ : ∀ ⦃a : α⦄ {s : multiset α}, p sp (a ::ₘ s)) (s : multiset α) :
p s

theorem multiset.induction_on {α : Type u_1} {p : multiset α → Prop} (s : multiset α) :
p 0(∀ ⦃a : α⦄ {s : multiset α}, p sp (a ::ₘ s))p s

theorem multiset.cons_swap {α : Type u_1} (a b : α) (s : multiset α) :
a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s

def multiset.rec {α : Type u_1} {C : multiset αSort u_4} (C_0 : C 0) (C_cons : Π (a : α) (m : multiset α), C mC (a ::ₘ m)) (C_cons_heq : ∀ (a a' : α) (m : multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) == C_cons a' (a ::ₘ m) (C_cons a m b)) (m : multiset α) :
C m

Dependent recursor on multisets.

TODO: should be @[recursor 6], but then the definition of multiset.pi fails with a stack overflow in whnf.

Equations
def multiset.rec_on {α : Type u_1} {C : multiset αSort u_4} (m : multiset α) (C_0 : C 0) (C_cons : Π (a : α) (m : multiset α), C mC (a ::ₘ m)) :
(∀ (a a' : α) (m : multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) == C_cons a' (a ::ₘ m) (C_cons a m b))C m

Equations
@[simp]
theorem multiset.rec_on_0 {α : Type u_1} {C : multiset αSort u_4} {C_0 : C 0} {C_cons : Π (a : α) (m : multiset α), C mC (a ::ₘ m)} {C_cons_heq : ∀ (a a' : α) (m : multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) == C_cons a' (a ::ₘ m) (C_cons a m b)} :
0.rec_on C_0 C_cons C_cons_heq = C_0

@[simp]
theorem multiset.rec_on_cons {α : Type u_1} {C : multiset αSort u_4} {C_0 : C 0} {C_cons : Π (a : α) (m : multiset α), C mC (a ::ₘ m)} {C_cons_heq : ∀ (a a' : α) (m : multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) == C_cons a' (a ::ₘ m) (C_cons a m b)} (a : α) (m : multiset α) :
(a ::ₘ m).rec_on C_0 C_cons C_cons_heq = C_cons a m (m.rec_on C_0 C_cons C_cons_heq)

def multiset.mem {α : Type u_1} :
α → multiset α → Prop

a ∈ s means that a has nonzero multiplicity in s.

Equations
@[instance]
def multiset.has_mem {α : Type u_1} :

Equations
@[simp]
theorem multiset.mem_coe {α : Type u_1} {a : α} {l : list α} :
a l a l

@[instance]
def multiset.decidable_mem {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

Equations
@[simp]
theorem multiset.mem_cons {α : Type u_1} {a b : α} {s : multiset α} :
a b ::ₘ s a = b a s

theorem multiset.mem_cons_of_mem {α : Type u_1} {a b : α} {s : multiset α} :
a sa b ::ₘ s

@[simp]
theorem multiset.mem_cons_self {α : Type u_1} (a : α) (s : multiset α) :
a a ::ₘ s

theorem multiset.forall_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {s : multiset α} :
(∀ (x : α), x a ::ₘ sp x) p a ∀ (x : α), x sp x

theorem multiset.exists_cons_of_mem {α : Type u_1} {s : multiset α} {a : α} :
a s(∃ (t : multiset α), s = a ::ₘ t)

@[simp]
theorem multiset.not_mem_zero {α : Type u_1} (a : α) :
a 0

theorem multiset.eq_zero_of_forall_not_mem {α : Type u_1} {s : multiset α} :
(∀ (x : α), x s)s = 0

theorem multiset.eq_zero_iff_forall_not_mem {α : Type u_1} {s : multiset α} :
s = 0 ∀ (a : α), a s

theorem multiset.exists_mem_of_ne_zero {α : Type u_1} {s : multiset α} :
s 0(∃ (a : α), a s)

@[simp]
theorem multiset.zero_ne_cons {α : Type u_1} {a : α} {m : multiset α} :
0 a ::ₘ m

@[simp]
theorem multiset.cons_ne_zero {α : Type u_1} {a : α} {m : multiset α} :
a ::ₘ m 0

theorem multiset.cons_eq_cons {α : Type u_1} {a b : α} {as bs : multiset α} :
a ::ₘ as = b ::ₘ bs a = b as = bs a b ∃ (cs : multiset α), as = b ::ₘ cs bs = a ::ₘ cs

def multiset.subset {α : Type u_1} :
multiset αmultiset α → Prop

s ⊆ t is the lift of the list subset relation. It means that any element with nonzero multiplicity in s has nonzero multiplicity in t, but it does not imply that the multiplicity of a in s is less or equal than in t; see s ≤ t for this relation.

Equations
@[instance]
def multiset.has_subset {α : Type u_1} :

Equations
@[simp]
theorem multiset.coe_subset {α : Type u_1} {l₁ l₂ : list α} :
l₁ l₂ l₁ l₂

@[simp]
theorem multiset.subset.refl {α : Type u_1} (s : multiset α) :
s s

theorem multiset.subset.trans {α : Type u_1} {s t u : multiset α} :
s tt us u

theorem multiset.subset_iff {α : Type u_1} {s t : multiset α} :
s t ∀ ⦃x : α⦄, x sx t

theorem multiset.mem_of_subset {α : Type u_1} {s t : multiset α} {a : α} :
s ta sa t

@[simp]
theorem multiset.zero_subset {α : Type u_1} (s : multiset α) :
0 s

@[simp]
theorem multiset.cons_subset {α : Type u_1} {a : α} {s t : multiset α} :
a ::ₘ s t a t s t

theorem multiset.eq_zero_of_subset_zero {α : Type u_1} {s : multiset α} :
s 0s = 0

theorem multiset.subset_zero {α : Type u_1} {s : multiset α} :
s 0 s = 0

def multiset.to_list {α : Type u_1} :
multiset αlist α

Produces a list of the elements in the multiset using choice.

Equations
@[simp]
theorem multiset.to_list_zero {α : Type u_1} :

theorem multiset.coe_to_list {α : Type u_1} (s : multiset α) :

theorem multiset.mem_to_list {α : Type u_1} (a : α) (s : multiset α) :
a s.to_list a s

def multiset.le {α : Type u_1} :
multiset αmultiset α → Prop

s ≤ t means that s is a sublist of t (up to permutation). Equivalently, s ≤ t means that count a s ≤ count a t for all a.

Equations
@[instance]
def multiset.partial_order {α : Type u_1} :

Equations
theorem multiset.subset_of_le {α : Type u_1} {s t : multiset α} :
s ts t

theorem multiset.mem_of_le {α : Type u_1} {s t : multiset α} {a : α} :
s ta sa t

@[simp]
theorem multiset.coe_le {α : Type u_1} {l₁ l₂ : list α} :
l₁ l₂ l₁ <+~ l₂

theorem multiset.le_induction_on {α : Type u_1} {C : multiset αmultiset α → Prop} {s t : multiset α} :
s t(∀ {l₁ l₂ : list α}, l₁ <+ l₂C l₁ l₂)C s t

theorem multiset.zero_le {α : Type u_1} (s : multiset α) :
0 s

theorem multiset.le_zero {α : Type u_1} {s : multiset α} :
s 0 s = 0

theorem multiset.lt_cons_self {α : Type u_1} (s : multiset α) (a : α) :
s < a ::ₘ s

theorem multiset.le_cons_self {α : Type u_1} (s : multiset α) (a : α) :
s a ::ₘ s

theorem multiset.cons_le_cons_iff {α : Type u_1} (a : α) {s t : multiset α} :
a ::ₘ s a ::ₘ t s t

theorem multiset.cons_le_cons {α : Type u_1} (a : α) {s t : multiset α} :
s ta ::ₘ s a ::ₘ t

theorem multiset.le_cons_of_not_mem {α : Type u_1} {a : α} {s t : multiset α} :
a s(s a ::ₘ t s t)

def multiset.card {α : Type u_1} :
multiset α

The cardinality of a multiset is the sum of the multiplicities of all its elements, or simply the length of the underlying list.

Equations
@[simp]
theorem multiset.coe_card {α : Type u_1} (l : list α) :

@[simp]
theorem multiset.card_zero {α : Type u_1} :
0.card = 0

@[simp]
theorem multiset.card_cons {α : Type u_1} (a : α) (s : multiset α) :
(a ::ₘ s).card = s.card + 1

@[simp]
theorem multiset.card_singleton {α : Type u_1} (a : α) :
(a ::ₘ 0).card = 1

theorem multiset.card_le_of_le {α : Type u_1} {s t : multiset α} :
s ts.card t.card

theorem multiset.eq_of_le_of_card_le {α : Type u_1} {s t : multiset α} :
s tt.card s.cards = t

theorem multiset.card_lt_of_lt {α : Type u_1} {s t : multiset α} :
s < ts.card < t.card

theorem multiset.lt_iff_cons_le {α : Type u_1} {s t : multiset α} :
s < t ∃ (a : α), a ::ₘ s t

@[simp]
theorem multiset.card_eq_zero {α : Type u_1} {s : multiset α} :
s.card = 0 s = 0

theorem multiset.card_pos {α : Type u_1} {s : multiset α} :
0 < s.card s 0

theorem multiset.card_pos_iff_exists_mem {α : Type u_1} {s : multiset α} :
0 < s.card ∃ (a : α), a s

def multiset.strong_induction_on {α : Type u_1} {p : multiset αSort u_2} (s : multiset α) :
(Π (s : multiset α), (Π (t : multiset α), t < sp t)p s)p s

Equations
theorem multiset.strong_induction_eq {α : Type u_1} {p : multiset αSort u_2} (s : multiset α) (H : Π (s : multiset α), (Π (t : multiset α), t < sp t)p s) :
s.strong_induction_on H = H s (λ (t : multiset α) (h : t < s), t.strong_induction_on H)

theorem multiset.case_strong_induction_on {α : Type u_1} {p : multiset α → Prop} (s : multiset α) :
p 0(∀ (a : α) (s : multiset α), (∀ (t : multiset α), t sp t)p (a ::ₘ s))p s

@[instance]
def multiset.has_singleton {α : Type u_1} :

Equations
@[simp]
theorem multiset.singleton_eq_singleton {α : Type u_1} (a : α) :
{a} = a ::ₘ 0

@[simp]
theorem multiset.mem_singleton {α : Type u_1} {a b : α} :
b a ::ₘ 0 b = a

theorem multiset.mem_singleton_self {α : Type u_1} (a : α) :
a a ::ₘ 0

theorem multiset.singleton_inj {α : Type u_1} {a b : α} :
a ::ₘ 0 = b ::ₘ 0 a = b

@[simp]
theorem multiset.singleton_ne_zero {α : Type u_1} (a : α) :
a ::ₘ 0 0

@[simp]
theorem multiset.singleton_le {α : Type u_1} {a : α} {s : multiset α} :
a ::ₘ 0 s a s

theorem multiset.card_eq_one {α : Type u_1} {s : multiset α} :
s.card = 1 ∃ (a : α), s = a ::ₘ 0

def multiset.add {α : Type u_1} :
multiset αmultiset αmultiset α

The sum of two multisets is the lift of the list append operation. This adds the multiplicities of each element, i.e. count a (s + t) = count a s + count a t.

Equations
@[instance]
def multiset.has_add {α : Type u_1} :

Equations
@[simp]
theorem multiset.coe_add {α : Type u_1} (s t : list α) :
s + t = (s ++ t)

theorem multiset.add_comm {α : Type u_1} (s t : multiset α) :
s + t = t + s

theorem multiset.zero_add {α : Type u_1} (s : multiset α) :
0 + s = s

theorem multiset.singleton_add {α : Type u_1} (a : α) (s : multiset α) :
[a] + s = a ::ₘ s

theorem multiset.add_le_add_left {α : Type u_1} (s : multiset α) {t u : multiset α} :
s + t s + u t u

theorem multiset.add_left_cancel {α : Type u_1} (s : multiset α) {t u : multiset α} :
s + t = s + ut = u

@[simp]
theorem multiset.cons_add {α : Type u_1} (a : α) (s t : multiset α) :
a ::ₘ s + t = a ::ₘ (s + t)

@[simp]
theorem multiset.add_cons {α : Type u_1} (a : α) (s t : multiset α) :
s + a ::ₘ t = a ::ₘ (s + t)

theorem multiset.le_add_right {α : Type u_1} (s t : multiset α) :
s s + t

theorem multiset.le_add_left {α : Type u_1} (s t : multiset α) :
s t + s

@[simp]
theorem multiset.card_add {α : Type u_1} (s t : multiset α) :
(s + t).card = s.card + t.card

theorem multiset.card_smul {α : Type u_1} (s : multiset α) (n : ) :
(n •ℕ s).card = n * s.card

@[simp]
theorem multiset.mem_add {α : Type u_1} {a : α} {s t : multiset α} :
a s + t a s a t

theorem multiset.le_iff_exists_add {α : Type u_1} {s t : multiset α} :
s t ∃ (u : multiset α), t = s + u

def multiset.repeat {α : Type u_1} :
α → multiset α

repeat a n is the multiset containing only a with multiplicity n.

Equations
@[simp]
theorem multiset.repeat_zero {α : Type u_1} (a : α) :

@[simp]
theorem multiset.repeat_succ {α : Type u_1} (a : α) (n : ) :

@[simp]
theorem multiset.repeat_one {α : Type u_1} (a : α) :

@[simp]
theorem multiset.card_repeat {α : Type u_1} (a : α) (n : ) :

theorem multiset.eq_of_mem_repeat {α : Type u_1} {a b : α} {n : } :
b multiset.repeat a nb = a

theorem multiset.eq_repeat' {α : Type u_1} {a : α} {s : multiset α} :
s = multiset.repeat a s.card ∀ (b : α), b sb = a

theorem multiset.eq_repeat_of_mem {α : Type u_1} {a : α} {s : multiset α} :
(∀ (b : α), b sb = a)s = multiset.repeat a s.card

theorem multiset.eq_repeat {α : Type u_1} {a : α} {n : } {s : multiset α} :
s = multiset.repeat a n s.card = n ∀ (b : α), b sb = a

theorem multiset.repeat_subset_singleton {α : Type u_1} (a : α) (n : ) :

theorem multiset.repeat_le_coe {α : Type u_1} {a : α} {n : } {l : list α} :

def multiset.erase {α : Type u_1} [decidable_eq α] :
multiset αα → multiset α

erase s a is the multiset that subtracts 1 from the multiplicity of a.

Equations
@[simp]
theorem multiset.coe_erase {α : Type u_1} [decidable_eq α] (l : list α) (a : α) :
l.erase a = (l.erase a)

@[simp]
theorem multiset.erase_zero {α : Type u_1} [decidable_eq α] (a : α) :
0.erase a = 0

@[simp]
theorem multiset.erase_cons_head {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :
(a ::ₘ s).erase a = s

@[simp]
theorem multiset.erase_cons_tail {α : Type u_1} [decidable_eq α] {a b : α} (s : multiset α) :
b a(b ::ₘ s).erase a = b ::ₘ s.erase a

@[simp]
theorem multiset.erase_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a ss.erase a = s

@[simp]
theorem multiset.cons_erase {α : Type u_1} [decidable_eq α] {s : multiset α} {a : α} :
a sa ::ₘ s.erase a = s

theorem multiset.le_cons_erase {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :
s a ::ₘ s.erase a

theorem multiset.erase_add_left_pos {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (t : multiset α) :
a s(s + t).erase a = s.erase a + t

theorem multiset.erase_add_right_pos {α : Type u_1} [decidable_eq α] {a : α} (s : multiset α) {t : multiset α} :
a t(s + t).erase a = s + t.erase a

theorem multiset.erase_add_right_neg {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (t : multiset α) :
a s(s + t).erase a = s + t.erase a

theorem multiset.erase_add_left_neg {α : Type u_1} [decidable_eq α] {a : α} (s : multiset α) {t : multiset α} :
a t(s + t).erase a = s.erase a + t

theorem multiset.erase_le {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :
s.erase a s

@[simp]
theorem multiset.erase_lt {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
s.erase a < s a s

theorem multiset.erase_subset {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :
s.erase a s

theorem multiset.mem_erase_of_ne {α : Type u_1} [decidable_eq α] {a b : α} {s : multiset α} :
a b(a s.erase b a s)

theorem multiset.mem_of_mem_erase {α : Type u_1} [decidable_eq α] {a b : α} {s : multiset α} :
a s.erase ba s

theorem multiset.erase_comm {α : Type u_1} [decidable_eq α] (s : multiset α) (a b : α) :
(s.erase a).erase b = (s.erase b).erase a

theorem multiset.erase_le_erase {α : Type u_1} [decidable_eq α] {s t : multiset α} (a : α) :
s ts.erase a t.erase a

theorem multiset.erase_le_iff_le_cons {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :
s.erase a t s a ::ₘ t

@[simp]
theorem multiset.card_erase_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a s(s.erase a).card = s.card.pred

theorem multiset.card_erase_lt_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a s(s.erase a).card < s.card

theorem multiset.card_erase_le {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
(s.erase a).card s.card

@[simp]
theorem multiset.coe_reverse {α : Type u_1} (l : list α) :

def multiset.map {α : Type u_1} {β : Type u_2} :
(α → β)multiset αmultiset β

map f s is the lift of the list map operation. The multiplicity of b in map f s is the number of a ∈ s (counting multiplicity) such that f a = b.

Equations
theorem multiset.forall_mem_map_iff {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Prop} {s : multiset α} :
(∀ (y : β), y multiset.map f sp y) ∀ (x : α), x sp (f x)

@[simp]
theorem multiset.coe_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : list α) :

@[simp]
theorem multiset.map_zero {α : Type u_1} {β : Type u_2} (f : α → β) :

@[simp]
theorem multiset.map_cons {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (s : multiset α) :

theorem multiset.map_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
multiset.map f {a} = {f a}

theorem multiset.map_repeat {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (k : ) :

@[simp]
theorem multiset.map_add {α : Type u_1} {β : Type u_2} (f : α → β) (s t : multiset α) :

@[instance]
def multiset.is_add_monoid_hom {α : Type u_1} {β : Type u_2} (f : α → β) :

theorem multiset.map_nsmul {α : Type u_1} {β : Type u_2} (f : α → β) (n : ) (s : multiset α) :

@[simp]
theorem multiset.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : multiset α} :
b multiset.map f s ∃ (a : α), a s f a = b

@[simp]
theorem multiset.card_map {α : Type u_1} {β : Type u_2} (f : α → β) (s : multiset α) :

@[simp]
theorem multiset.map_eq_zero {α : Type u_1} {β : Type u_2} {s : multiset α} {f : α → β} :
multiset.map f s = 0 s = 0

theorem multiset.mem_map_of_mem {α : Type u_1} {β : Type u_2} (f : α → β) {a : α} {s : multiset α} :
a sf a multiset.map f s

theorem multiset.mem_map_of_injective {α : Type u_1} {β : Type u_2} {f : α → β} (H : function.injective f) {a : α} {s : multiset α} :
f a multiset.map f s a s

@[simp]
theorem multiset.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (s : multiset α) :

theorem multiset.map_id {α : Type u_1} (s : multiset α) :

@[simp]
theorem multiset.map_id' {α : Type u_1} (s : multiset α) :
multiset.map (λ (x : α), x) s = s

@[simp]
theorem multiset.map_const {α : Type u_1} {β : Type u_2} (s : multiset α) (b : β) :

theorem multiset.map_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {s : multiset α} :
(∀ (x : α), x sf x = g x)multiset.map f s = multiset.map g s

theorem multiset.map_hcongr {α : Type u_1} {β β' : Type u_2} {m : multiset α} {f : α → β} {f' : α → β'} :
β = β'(∀ (a : α), a mf a == f' a)multiset.map f m == multiset.map f' m

theorem multiset.eq_of_mem_map_const {α : Type u_1} {β : Type u_2} {b₁ b₂ : β} {l : list α} :
b₁ multiset.map (function.const α b₂) lb₁ = b₂

@[simp]
theorem multiset.map_le_map {α : Type u_1} {β : Type u_2} {f : α → β} {s t : multiset α} :

@[simp]
theorem multiset.map_subset_map {α : Type u_1} {β : Type u_2} {f : α → β} {s t : multiset α} :

def multiset.foldl {α : Type u_1} {β : Type u_2} (f : β → α → β) :
right_commutative fβ → multiset α → β

foldl f H b s is the lift of the list operation foldl f b l, which folds f over the multiset. It is well defined when f is right-commutative, that is, f (f b a₁) a₂ = f (f b a₂) a₁.

Equations
@[simp]
theorem multiset.foldl_zero {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) :
multiset.foldl f H b 0 = b

@[simp]
theorem multiset.foldl_cons {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) (a : α) (s : multiset α) :
multiset.foldl f H b (a ::ₘ s) = multiset.foldl f H (f b a) s

@[simp]
theorem multiset.foldl_add {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) (s t : multiset α) :
multiset.foldl f H b (s + t) = multiset.foldl f H (multiset.foldl f H b s) t

def multiset.foldr {α : Type u_1} {β : Type u_2} (f : α → β → β) :
left_commutative fβ → multiset α → β

foldr f H b s is the lift of the list operation foldr f b l, which folds f over the multiset. It is well defined when f is left-commutative, that is, f a₁ (f a₂ b) = f a₂ (f a₁ b).

Equations
@[simp]
theorem multiset.foldr_zero {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) :
multiset.foldr f H b 0 = b

@[simp]
theorem multiset.foldr_cons {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (a : α) (s : multiset α) :
multiset.foldr f H b (a ::ₘ s) = f a (multiset.foldr f H b s)

@[simp]
theorem multiset.foldr_add {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (s t : multiset α) :
multiset.foldr f H b (s + t) = multiset.foldr f H (multiset.foldr f H b t) s

@[simp]
theorem multiset.coe_foldr {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (l : list α) :

@[simp]
theorem multiset.coe_foldl {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) (l : list α) :

theorem multiset.coe_foldr_swap {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (l : list α) :
multiset.foldr f H b l = list.foldl (λ (x : β) (y : α), f y x) b l

theorem multiset.foldr_swap {α : Type u_1} {β : Type u_2} (f : α → β → β) (H : left_commutative f) (b : β) (s : multiset α) :
multiset.foldr f H b s = multiset.foldl (λ (x : β) (y : α), f y x) _ b s

theorem multiset.foldl_swap {α : Type u_1} {β : Type u_2} (f : β → α → β) (H : right_commutative f) (b : β) (s : multiset α) :
multiset.foldl f H b s = multiset.foldr (λ (x : α) (y : β), f y x) _ b s

def multiset.sum {α : Type u_1} [add_comm_monoid α] :
multiset α → α

def multiset.prod {α : Type u_1} [comm_monoid α] :
multiset α → α

Product of a multiset given a commutative monoid structure on α. prod {a, b, c} = a * b * c

Equations
theorem multiset.sum_eq_foldr {α : Type u_1} [add_comm_monoid α] (s : multiset α) :

theorem multiset.prod_eq_foldr {α : Type u_1} [comm_monoid α] (s : multiset α) :

theorem multiset.prod_eq_foldl {α : Type u_1} [comm_monoid α] (s : multiset α) :

theorem multiset.sum_eq_foldl {α : Type u_1} [add_comm_monoid α] (s : multiset α) :

@[simp]
theorem multiset.coe_sum {α : Type u_1} [add_comm_monoid α] (l : list α) :

@[simp]
theorem multiset.coe_prod {α : Type u_1} [comm_monoid α] (l : list α) :

@[simp]
theorem multiset.prod_zero {α : Type u_1} [comm_monoid α] :
0.prod = 1

@[simp]
theorem multiset.sum_zero {α : Type u_1} [add_comm_monoid α] :
0.sum = 0

@[simp]
theorem multiset.prod_cons {α : Type u_1} [comm_monoid α] (a : α) (s : multiset α) :
(a ::ₘ s).prod = a * s.prod

@[simp]
theorem multiset.sum_cons {α : Type u_1} [add_comm_monoid α] (a : α) (s : multiset α) :
(a ::ₘ s).sum = a + s.sum

theorem multiset.prod_singleton {α : Type u_1} [comm_monoid α] (a : α) :
(a ::ₘ 0).prod = a

theorem multiset.sum_singleton {α : Type u_1} [add_comm_monoid α] (a : α) :
(a ::ₘ 0).sum = a

@[simp]
theorem multiset.prod_add {α : Type u_1} [comm_monoid α] (s t : multiset α) :
(s + t).prod = (s.prod) * t.prod

@[simp]
theorem multiset.sum_add {α : Type u_1} [add_comm_monoid α] (s t : multiset α) :
(s + t).sum = s.sum + t.sum

theorem multiset.prod_smul {α : Type u_1} [comm_monoid α] (m : multiset α) (n : ) :
(n •ℕ m).prod = m.prod ^ n

@[simp]
theorem multiset.prod_repeat {α : Type u_1} [comm_monoid α] (a : α) (n : ) :

@[simp]
theorem multiset.sum_repeat {α : Type u_1} [add_comm_monoid α] (a : α) (n : ) :

theorem multiset.prod_map_one {α : Type u_1} {γ : Type u_3} [comm_monoid γ] {m : multiset α} :
(multiset.map (λ (a : α), 1) m).prod = 1

theorem multiset.sum_map_zero {α : Type u_1} {γ : Type u_3} [add_comm_monoid γ] {m : multiset α} :
(multiset.map (λ (a : α), 0) m).sum = 0

@[simp]
theorem multiset.sum_map_add {α : Type u_1} {γ : Type u_3} [add_comm_monoid γ] {m : multiset α} {f g : α → γ} :
(multiset.map (λ (a : α), f a + g a) m).sum = (multiset.map f m).sum + (multiset.map g m).sum

@[simp]
theorem multiset.prod_map_mul {α : Type u_1} {γ : Type u_3} [comm_monoid γ] {m : multiset α} {f g : α → γ} :
(multiset.map (λ (a : α), (f a) * g a) m).prod = ((multiset.map f m).prod) * (multiset.map g m).prod

theorem multiset.prod_map_prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [comm_monoid γ] (m : multiset α) (n : multiset β) {f : α → β → γ} :
(multiset.map (λ (a : α), (multiset.map (λ (b : β), f a b) n).prod) m).prod = (multiset.map (λ (b : β), (multiset.map (λ (a : α), f a b) m).prod) n).prod

theorem multiset.sum_map_sum_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid γ] (m : multiset α) (n : multiset β) {f : α → β → γ} :
(multiset.map (λ (a : α), (multiset.map (λ (b : β), f a b) n).sum) m).sum = (multiset.map (λ (b : β), (multiset.map (λ (a : α), f a b) m).sum) n).sum

theorem multiset.sum_map_mul_left {α : Type u_1} {β : Type u_2} [semiring β] {b : β} {s : multiset α} {f : α → β} :
(multiset.map (λ (a : α), b * f a) s).sum = b * (multiset.map f s).sum

theorem multiset.sum_map_mul_right {α : Type u_1} {β : Type u_2} [semiring β] {b : β} {s : multiset α} {f : α → β} :
(multiset.map (λ (a : α), (f a) * b) s).sum = ((multiset.map f s).sum) * b

theorem multiset.prod_ne_zero {R : Type u_1} [integral_domain R] {m : multiset R} :
(∀ (x : R), x mx 0)m.prod 0

theorem multiset.prod_eq_zero {α : Type u_1} [comm_semiring α] {s : multiset α} :
0 ss.prod = 0

theorem multiset.sum_hom {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [add_comm_monoid β] (s : multiset α) (f : α →+ β) :

theorem multiset.prod_hom {α : Type u_1} {β : Type u_2} [comm_monoid α] [comm_monoid β] (s : multiset α) (f : α →* β) :

theorem multiset.sum_hom_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid β] [add_comm_monoid γ] (s : multiset α) {r : β → γ → Prop} {f : α → β} {g : α → γ} :
r 0 0(∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b cr (f a + b) (g a + c))r (multiset.map f s).sum (multiset.map g s).sum

theorem multiset.prod_hom_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [comm_monoid β] [comm_monoid γ] (s : multiset α) {r : β → γ → Prop} {f : α → β} {g : α → γ} :
r 1 1(∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b cr ((f a) * b) ((g a) * c))r (multiset.map f s).prod (multiset.map g s).prod

theorem multiset.dvd_prod {α : Type u_1} [comm_monoid α] {a : α} {s : multiset α} :
a sa s.prod

theorem multiset.prod_eq_zero_iff {α : Type u_1} [comm_cancel_monoid_with_zero α] [nontrivial α] {s : multiset α} :
s.prod = 0 0 s

theorem multiset.sum_nonneg {α : Type u_1} [ordered_add_comm_monoid α] {m : multiset α} :
(∀ (x : α), x m0 x)0 m.sum

theorem multiset.one_le_prod_of_one_le {α : Type u_1} [ordered_comm_monoid α] {m : multiset α} :
(∀ (x : α), x m1 x)1 m.prod

theorem multiset.single_le_prod {α : Type u_1} [ordered_comm_monoid α] {m : multiset α} (a : ∀ (x : α), x m1 x) (x : α) :
x mx m.prod

theorem multiset.single_le_sum {α : Type u_1} [ordered_add_comm_monoid α] {m : multiset α} (a : ∀ (x : α), x m0 x) (x : α) :
x mx m.sum

theorem multiset.all_one_of_le_one_le_of_prod_eq_one {α : Type u_1} [ordered_comm_monoid α] {m : multiset α} (a : ∀ (x : α), x m1 x) (a_1 : m.prod = 1) (x : α) :
x mx = 1

theorem multiset.all_zero_of_le_zero_le_of_sum_eq_zero {α : Type u_1} [ordered_add_comm_monoid α] {m : multiset α} (a : ∀ (x : α), x m0 x) (a_1 : m.sum = 0) (x : α) :
x mx = 0

theorem multiset.sum_eq_zero_iff {α : Type u_1} [canonically_ordered_add_monoid α] {m : multiset α} :
m.sum = 0 ∀ (x : α), x mx = 0

theorem multiset.le_sum_of_subadditive {α : Type u_1} {β : Type u_2} [add_comm_monoid α] [ordered_add_comm_monoid β] (f : α → β) (h_zero : f 0 = 0) (h_add : ∀ (x y : α), f (x + y) f x + f y) (s : multiset α) :

theorem multiset.dvd_sum {α : Type u_1} [comm_semiring α] {a : α} {s : multiset α} :
(∀ (x : α), x sa x)a s.sum

@[simp]
theorem multiset.sum_map_singleton {α : Type u_1} (s : multiset α) :
(multiset.map (λ (a : α), a ::ₘ 0) s).sum = s

Join

def multiset.join {α : Type u_1} :

join S, where S is a multiset of multisets, is the lift of the list join operation, that is, the union of all the sets.

join {{1, 2}, {1, 2}, {0, 1}} = {0, 1, 1, 1, 2, 2}
Equations
theorem multiset.coe_join {α : Type u_1} (L : list (list α)) :

@[simp]
theorem multiset.join_zero {α : Type u_1} :
0.join = 0

@[simp]
theorem multiset.join_cons {α : Type u_1} (s : multiset α) (S : multiset (multiset α)) :
(s ::ₘ S).join = s + S.join

@[simp]
theorem multiset.join_add {α : Type u_1} (S T : multiset (multiset α)) :
(S + T).join = S.join + T.join

@[simp]
theorem multiset.mem_join {α : Type u_1} {a : α} {S : multiset (multiset α)} :
a S.join ∃ (s : multiset α) (H : s S), a s

@[simp]
theorem multiset.card_join {α : Type u_1} (S : multiset (multiset α)) :

def multiset.bind {α : Type u_1} {β : Type u_2} :
multiset α(α → multiset β)multiset β

bind s f is the monad bind operation, defined as join (map f s). It is the union of f a as a ranges over s.

Equations
@[simp]
theorem multiset.coe_bind {α : Type u_1} {β : Type u_2} (l : list α) (f : α → list β) :
l.bind (λ (a : α), (f a)) = (l.bind f)

@[simp]
theorem multiset.zero_bind {α : Type u_1} {β : Type u_2} (f : α → multiset β) :
0.bind f = 0

@[simp]
theorem multiset.cons_bind {α : Type u_1} {β : Type u_2} (a : α) (s : multiset α) (f : α → multiset β) :
(a ::ₘ s).bind f = f a + s.bind f

@[simp]
theorem multiset.add_bind {α : Type u_1} {β : Type u_2} (s t : multiset α) (f : α → multiset β) :
(s + t).bind f = s.bind f + t.bind f

@[simp]
theorem multiset.bind_zero {α : Type u_1} {β : Type u_2} (s : multiset α) :
s.bind (λ (a : α), 0) = 0

@[simp]
theorem multiset.bind_add {α : Type u_1} {β : Type u_2} (s : multiset α) (f g : α → multiset β) :
s.bind (λ (a : α), f a + g a) = s.bind f + s.bind g

@[simp]
theorem multiset.bind_cons {α : Type u_1} {β : Type u_2} (s : multiset α) (f : α → β) (g : α → multiset β) :
s.bind (λ (a : α), f a ::ₘ g a) = multiset.map f s + s.bind g

@[simp]
theorem multiset.mem_bind {α : Type u_1} {β : Type u_2} {b : β} {s : multiset α} {f : α → multiset β} :
b s.bind f ∃ (a : α) (H : a s), b f a

@[simp]
theorem multiset.card_bind {α : Type u_1} {β : Type u_2} (s : multiset α) (f : α → multiset β) :

theorem multiset.bind_congr {α : Type u_1} {β : Type u_2} {f g : α → multiset β} {m : multiset α} :
(∀ (a : α), a mf a = g a)m.bind f = m.bind g

theorem multiset.bind_hcongr {α : Type u_1} {β β' : Type u_2} {m : multiset α} {f : α → multiset β} {f' : α → multiset β'} :
β = β'(∀ (a : α), a mf a == f' a)m.bind f == m.bind f'

theorem multiset.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : multiset α) (n : α → multiset β) (f : β → γ) :
multiset.map f (m.bind n) = m.bind (λ (a : α), multiset.map f (n a))

theorem multiset.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : multiset α) (n : β → multiset γ) (f : α → β) :
(multiset.map f m).bind n = m.bind (λ (a : α), n (f a))

theorem multiset.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : multiset α} {f : α → multiset β} {g : β → multiset γ} :
(s.bind f).bind g = s.bind (λ (a : α), (f a).bind g)

theorem multiset.bind_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : multiset α) (n : multiset β) {f : α → β → multiset γ} :
m.bind (λ (a : α), n.bind (λ (b : β), f a b)) = n.bind (λ (b : β), m.bind (λ (a : α), f a b))

theorem multiset.bind_map_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : multiset α) (n : multiset β) {f : α → β → γ} :
m.bind (λ (a : α), multiset.map (λ (b : β), f a b) n) = n.bind (λ (b : β), multiset.map (λ (a : α), f a b) m)

@[simp]
theorem multiset.prod_bind {α : Type u_1} {β : Type u_2} [comm_monoid β] (s : multiset α) (t : α → multiset β) :
(s.bind t).prod = (multiset.map (λ (a : α), (t a).prod) s).prod

@[simp]
theorem multiset.sum_bind {α : Type u_1} {β : Type u_2} [add_comm_monoid β] (s : multiset α) (t : α → multiset β) :
(s.bind t).sum = (multiset.map (λ (a : α), (t a).sum) s).sum

def multiset.product {α : Type u_1} {β : Type u_2} :
multiset αmultiset βmultiset × β)

The multiplicity of (a, b) in product s t is the product of the multiplicity of a in s and b in t.

Equations
@[simp]
theorem multiset.coe_product {α : Type u_1} {β : Type u_2} (l₁ : list α) (l₂ : list β) :
l₁.product l₂ = (l₁.product l₂)

@[simp]
theorem multiset.zero_product {α : Type u_1} {β : Type u_2} (t : multiset β) :
0.product t = 0

@[simp]
theorem multiset.cons_product {α : Type u_1} {β : Type u_2} (a : α) (s : multiset α) (t : multiset β) :

@[simp]
theorem multiset.product_singleton {α : Type u_1} {β : Type u_2} (a : α) (b : β) :
(a ::ₘ 0).product (b ::ₘ 0) = (a, b) ::ₘ 0

@[simp]
theorem multiset.add_product {α : Type u_1} {β : Type u_2} (s t : multiset α) (u : multiset β) :
(s + t).product u = s.product u + t.product u

@[simp]
theorem multiset.product_add {α : Type u_1} {β : Type u_2} (s : multiset α) (t u : multiset β) :
s.product (t + u) = s.product t + s.product u

@[simp]
theorem multiset.mem_product {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} {p : α × β} :
p s.product t p.fst s p.snd t

@[simp]
theorem multiset.card_product {α : Type u_1} {β : Type u_2} (s : multiset α) (t : multiset β) :
(s.product t).card = (s.card) * t.card

def multiset.sigma {α : Type u_1} {σ : α → Type u_4} :
multiset α(Π (a : α), multiset (σ a))multiset (Σ (a : α), σ a)

sigma s t is the dependent version of product. It is the sum of (a, b) as a ranges over s and b ranges over t a.

Equations
@[simp]
theorem multiset.coe_sigma {α : Type u_1} {σ : α → Type u_4} (l₁ : list α) (l₂ : Π (a : α), list (σ a)) :
l₁.sigma (λ (a : α), (l₂ a)) = (l₁.sigma l₂)

@[simp]
theorem multiset.zero_sigma {α : Type u_1} {σ : α → Type u_4} (t : Π (a : α), multiset (σ a)) :
0.sigma t = 0

@[simp]
theorem multiset.cons_sigma {α : Type u_1} {σ : α → Type u_4} (a : α) (s : multiset α) (t : Π (a : α), multiset (σ a)) :
(a ::ₘ s).sigma t = multiset.map (sigma.mk a) (t a) + s.sigma t

@[simp]
theorem multiset.sigma_singleton {α : Type u_1} {β : Type u_2} (a : α) (b : α → β) :
(a ::ₘ 0).sigma (λ (a : α), b a ::ₘ 0) = a, b a ::ₘ 0

@[simp]
theorem multiset.add_sigma {α : Type u_1} {σ : α → Type u_4} (s t : multiset α) (u : Π (a : α), multiset (σ a)) :
(s + t).sigma u = s.sigma u + t.sigma u

@[simp]
theorem multiset.sigma_add {α : Type u_1} {σ : α → Type u_4} (s : multiset α) (t u : Π (a : α), multiset (σ a)) :
s.sigma (λ (a : α), t a + u a) = s.sigma t + s.sigma u

@[simp]
theorem multiset.mem_sigma {α : Type u_1} {σ : α → Type u_4} {s : multiset α} {t : Π (a : α), multiset (σ a)} {p : Σ (a : α), σ a} :
p s.sigma t p.fst s p.snd t p.fst

@[simp]
theorem multiset.card_sigma {α : Type u_1} {σ : α → Type u_4} (s : multiset α) (t : Π (a : α), multiset (σ a)) :
(s.sigma t).card = (multiset.map (λ (a : α), (t a).card) s).sum

def multiset.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (s : multiset α) :
(∀ (a : α), a sp a)multiset β

Lift of the list pmap operation. Map a partial function f over a multiset s whose elements are all in the domain of f.

Equations
@[simp]
theorem multiset.coe_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (l : list α) (H : ∀ (a : α), a lp a) :

@[simp]
theorem multiset.pmap_zero {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (h : ∀ (a : α), a 0p a) :

@[simp]
theorem multiset.pmap_cons {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (a : α) (m : multiset α) (h : ∀ (b : α), b a ::ₘ mp b) :
multiset.pmap f (a ::ₘ m) h = f a _ ::ₘ multiset.pmap f m _

def multiset.attach {α : Type u_1} (s : multiset α) :
multiset {x // x s}

"Attach" a proof that a ∈ s to each element a in s to produce a multiset on {x // x ∈ s}.

Equations
@[simp]
theorem multiset.coe_attach {α : Type u_1} (l : list α) :

theorem multiset.sizeof_lt_sizeof_of_mem {α : Type u_1} [has_sizeof α] {x : α} {s : multiset α} :
x ssizeof x < sizeof s

theorem multiset.pmap_eq_map {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : α → β) (s : multiset α) (H : ∀ (a : α), a sp a) :
multiset.pmap (λ (a : α) (_x : p a), f a) s H = multiset.map f s

theorem multiset.pmap_congr {α : Type u_1} {β : Type u_2} {p q : α → Prop} {f : Π (a : α), p a → β} {g : Π (a : α), q a → β} (s : multiset α) {H₁ : ∀ (a : α), a sp a} {H₂ : ∀ (a : α), a sq a} :
(∀ (a : α) (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂)multiset.pmap f s H₁ = multiset.pmap g s H₂

theorem multiset.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} (g : β → γ) (f : Π (a : α), p a → β) (s : multiset α) (H : ∀ (a : α), a sp a) :
multiset.map g (multiset.pmap f s H) = multiset.pmap (λ (a : α) (h : p a), g (f a h)) s H

theorem multiset.pmap_eq_map_attach {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (s : multiset α) (H : ∀ (a : α), a sp a) :
multiset.pmap f s H = multiset.map (λ (x : {x // x s}), f x.val _) s.attach

theorem multiset.attach_map_val {α : Type u_1} (s : multiset α) :

@[simp]
theorem multiset.mem_attach {α : Type u_1} (s : multiset α) (x : {x // x s}) :

@[simp]
theorem multiset.mem_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : Π (a : α), p a → β} {s : multiset α} {H : ∀ (a : α), a sp a} {b : β} :
b multiset.pmap f s H ∃ (a : α) (h : a s), f a _ = b

@[simp]
theorem multiset.card_pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (s : multiset α) (H : ∀ (a : α), a sp a) :

@[simp]
theorem multiset.card_attach {α : Type u_1} {m : multiset α} :

@[simp]
theorem multiset.attach_zero {α : Type u_1} :
0.attach = 0

theorem multiset.attach_cons {α : Type u_1} (a : α) (m : multiset α) :
(a ::ₘ m).attach = a, _⟩ ::ₘ multiset.map (λ (p : {x // x m}), p.val, _⟩) m.attach

def multiset.decidable_forall_multiset {α : Type u_1} {m : multiset α} {p : α → Prop} [hp : Π (a : α), decidable (p a)] :
decidable (∀ (a : α), a mp a)

Equations
@[instance]
def multiset.decidable_dforall_multiset {α : Type u_1} {m : multiset α} {p : Π (a : α), a m → Prop} [hp : Π (a : α) (h : a m), decidable (p a h)] :
decidable (∀ (a : α) (h : a m), p a h)

Equations
@[instance]
def multiset.decidable_eq_pi_multiset {α : Type u_1} {m : multiset α} {β : α → Type u_2} [h : Π (a : α), decidable_eq (β a)] :
decidable_eq (Π (a : α), a mβ a)

decidable equality for functions whose domain is bounded by multisets

Equations
@[instance]
def multiset.decidable_dexists_multiset {α : Type u_1} {m : multiset α} {p : Π (a : α), a m → Prop} [hp : Π (a : α) (h : a m), decidable (p a h)] :
decidable (∃ (a : α) (h : a m), p a h)

Equations
def multiset.sub {α : Type u_1} [decidable_eq α] :
multiset αmultiset αmultiset α

s - t is the multiset such that count a (s - t) = count a s - count a t for all a.

Equations
@[instance]
def multiset.has_sub {α : Type u_1} [decidable_eq α] :

Equations
@[simp]
theorem multiset.coe_sub {α : Type u_1} [decidable_eq α] (s t : list α) :
s - t = (s.diff t)

@[simp]
theorem multiset.sub_zero {α : Type u_1} [decidable_eq α] (s : multiset α) :
s - 0 = s

@[simp]
theorem multiset.sub_cons {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :
s - a ::ₘ t = s.erase a - t

theorem multiset.add_sub_of_le {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s ts + (t - s) = t

theorem multiset.sub_add' {α : Type u_1} [decidable_eq α] {s t u : multiset α} :
s - (t + u) = s - t - u

theorem multiset.sub_add_cancel {α : Type u_1} [decidable_eq α] {s t : multiset α} :
t ss - t + t = s

@[simp]
theorem multiset.add_sub_cancel_left {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s + t - s = t

@[simp]
theorem multiset.add_sub_cancel {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s + t - t = s

theorem multiset.sub_le_sub_right {α : Type u_1} [decidable_eq α] {s t : multiset α} (h : s t) (u : multiset α) :
s - u t - u

theorem multiset.sub_le_sub_left {α : Type u_1} [decidable_eq α] {s t : multiset α} (h : s t) (u : multiset α) :
u - t u - s

theorem multiset.sub_le_iff_le_add {α : Type u_1} [decidable_eq α] {s t u : multiset α} :
s - t u s u + t

theorem multiset.le_sub_add {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s s - t + t

theorem multiset.sub_le_self {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s - t s

@[simp]
theorem multiset.card_sub {α : Type u_1} [decidable_eq α] {s t : multiset α} :
t s(s - t).card = s.card - t.card

def multiset.union {α : Type u_1} [decidable_eq α] :
multiset αmultiset αmultiset α

s ∪ t is the lattice join operation with respect to the multiset . The multiplicity of a in s ∪ t is the maximum of the multiplicities in s and t.

Equations
@[instance]
def multiset.has_union {α : Type u_1} [decidable_eq α] :

Equations
theorem multiset.union_def {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s t = s - t + t

theorem multiset.le_union_left {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s s t

theorem multiset.le_union_right {α : Type u_1} [decidable_eq α] (s t : multiset α) :
t s t

theorem multiset.eq_union_left {α : Type u_1} [decidable_eq α] {s t : multiset α} :
t ss t = s

theorem multiset.union_le_union_right {α : Type u_1} [decidable_eq α] {s t : multiset α} (h : s t) (u : multiset α) :
s u t u

theorem multiset.union_le {α : Type u_1} [decidable_eq α] {s t u : multiset α} :
s ut us t u

@[simp]
theorem multiset.mem_union {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :
a s t a s a t

@[simp]
theorem multiset.map_union {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {f : α → β} (finj : function.injective f) {s t : multiset α} :

def multiset.inter {α : Type u_1} [decidable_eq α] :
multiset αmultiset αmultiset α

s ∩ t is the lattice meet operation with respect to the multiset . The multiplicity of a in s ∩ t is the minimum of the multiplicities in s and t.

Equations
@[instance]
def multiset.has_inter {α : Type u_1} [decidable_eq α] :

Equations
@[simp]
theorem multiset.inter_zero {α : Type u_1} [decidable_eq α] (s : multiset α) :
s 0 = 0

@[simp]
theorem multiset.zero_inter {α : Type u_1} [decidable_eq α] (s : multiset α) :
0 s = 0

@[simp]
theorem multiset.cons_inter_of_pos {α : Type u_1} [decidable_eq α] {a : α} (s : multiset α) {t : multiset α} :
a t(a ::ₘ s) t = a ::ₘ s t.erase a

@[simp]
theorem multiset.cons_inter_of_neg {α : Type u_1} [decidable_eq α] {a : α} (s : multiset α) {t : multiset α} :
a t(a ::ₘ s) t = s t

theorem multiset.inter_le_left {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s t s

theorem multiset.inter_le_right {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s t t

theorem multiset.le_inter {α : Type u_1} [decidable_eq α] {s t u : multiset α} :
s ts us t u

@[simp]
theorem multiset.mem_inter {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :
a s t a s a t

@[simp]
theorem multiset.sup_eq_union {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s t = s t

@[simp]
theorem multiset.inf_eq_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s t = s t

@[simp]
theorem multiset.le_inter_iff {α : Type u_1} [decidable_eq α] {s t u : multiset α} :
s t u s t s u

@[simp]
theorem multiset.union_le_iff {α : Type u_1} [decidable_eq α] {s t u : multiset α} :
s t u s u t u

theorem multiset.union_comm {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s t = t s

theorem multiset.inter_comm {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s t = t s

theorem multiset.eq_union_right {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s ts t = t

theorem multiset.union_le_union_left {α : Type u_1} [decidable_eq α] {s t : multiset α} (h : s t) (u : multiset α) :
u s u t

theorem multiset.union_le_add {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s t s + t

theorem multiset.union_add_distrib {α : Type u_1} [decidable_eq α] (s t u : multiset α) :
s t + u = s + u (t + u)

theorem multiset.add_union_distrib {α : Type u_1} [decidable_eq α] (s t u : multiset α) :
s + (t u) = s + t (s + u)

theorem multiset.cons_union_distrib {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :
a ::ₘ (s t) = a ::ₘ s a ::ₘ t

theorem multiset.inter_add_distrib {α : Type u_1} [decidable_eq α] (s t u : multiset α) :
s t + u = (s + u) (t + u)

theorem multiset.add_inter_distrib {α : Type u_1} [decidable_eq α] (s t u : multiset α) :
s + t u = (s + t) (s + u)

theorem multiset.cons_inter_distrib {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :
a ::ₘ s t = (a ::ₘ s) (a ::ₘ t)

theorem multiset.union_add_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s t + s t = s + t

theorem multiset.sub_add_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s - t + s t = s

theorem multiset.sub_inter {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s - s t = s - t

def multiset.filter {α : Type u_1} (p : α → Prop) [h : decidable_pred p] :
multiset αmultiset α

filter p s returns the elements in s (with the same multiplicities) which satisfy p, and removes the rest.

Equations
@[simp]
theorem multiset.coe_filter {α : Type u_1} (p : α → Prop) [h : decidable_pred p] (l : list α) :

@[simp]
theorem multiset.filter_zero {α : Type u_1} (p : α → Prop) [h : decidable_pred p] :

@[simp]
theorem multiset.filter_cons_of_pos {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} (s : multiset α) :

@[simp]
theorem multiset.filter_cons_of_neg {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} (s : multiset α) :

theorem multiset.filter_congr {α : Type u_1} {p q : α → Prop} [decidable_pred p] [decidable_pred q] {s : multiset α} :
(∀ (x : α), x s(p x q x))multiset.filter p s = multiset.filter q s

@[simp]
theorem multiset.filter_add {α : Type u_1} {p : α → Prop} [decidable_pred p] (s t : multiset α) :

@[simp]
theorem multiset.filter_le {α : Type u_1} {p : α → Prop} [decidable_pred p] (s : multiset α) :

@[simp]
theorem multiset.filter_subset {α : Type u_1} {p : α → Prop} [decidable_pred p] (s : multiset α) :

@[simp]
theorem multiset.mem_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} :
a multiset.filter p s a s p a

theorem multiset.of_mem_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} :
a multiset.filter p sp a

theorem multiset.mem_of_mem_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} :
a multiset.filter p sa s

theorem multiset.mem_filter_of_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} {l : multiset α} :
a lp aa multiset.filter p l

theorem multiset.filter_eq_self {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : multiset α} :
multiset.filter p s = s ∀ (a : α), a sp a

theorem multiset.filter_eq_nil {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : multiset α} :
multiset.filter p s = 0 ∀ (a : α), a s¬p a

theorem multiset.filter_le_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {s t : multiset α} :

theorem multiset.le_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {s t : multiset α} :
s multiset.filter p t s t ∀ (a : α), a sp a

@[simp]
theorem multiset.filter_sub {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] (s t : multiset α) :

@[simp]
theorem multiset.filter_union {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] (s t : multiset α) :

@[simp]
theorem multiset.filter_inter {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] (s t : multiset α) :

@[simp]
theorem multiset.filter_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {q : α → Prop} [decidable_pred q] (s : multiset α) :
multiset.filter p (multiset.filter q s) = multiset.filter (λ (a : α), p a q a) s

theorem multiset.filter_add_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {q : α → Prop} [decidable_pred q] (s : multiset α) :
multiset.filter p s + multiset.filter q s = multiset.filter (λ (a : α), p a q a) s + multiset.filter (λ (a : α), p a q a) s

theorem multiset.filter_add_not {α : Type u_1} {p : α → Prop} [decidable_pred p] (s : multiset α) :
multiset.filter p s + multiset.filter (λ (a : α), ¬p a) s = s

def multiset.filter_map {α : Type u_1} {β : Type u_2} :
(α → option β)multiset αmultiset β

filter_map f s is a combination filter/map operation on s. The function f : α → option β is applied to each element of s; if f a is some b then b is added to the result, otherwise a is removed from the resulting multiset.

Equations
@[simp]
theorem multiset.coe_filter_map {α : Type u_1} {β : Type u_2} (f : α → option β) (l : list α) :

@[simp]
theorem multiset.filter_map_zero {α : Type u_1} {β : Type u_2} (f : α → option β) :

@[simp]
theorem multiset.filter_map_cons_none {α : Type u_1} {β : Type u_2} {f : α → option β} (a : α) (s : multiset α) :

@[simp]
theorem multiset.filter_map_cons_some {α : Type u_1} {β : Type u_2} (f : α → option β) (a : α) (s : multiset α) {b : β} :

theorem multiset.filter_map_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) :

theorem multiset.filter_map_filter_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → option β) (g : β → option γ) (s : multiset α) :

theorem multiset.map_filter_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → option β) (g : β → γ) (s : multiset α) :

theorem multiset.filter_map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → option γ) (s : multiset α) :

theorem multiset.filter_filter_map {α : Type u_1} {β : Type u_2} (f : α → option β) (p : β → Prop) [decidable_pred p] (s : multiset α) :

theorem multiset.filter_map_filter {α : Type u_1} {β : Type u_2} (p : α → Prop) [decidable_pred p] (f : α → option β) (s : multiset α) :
multiset.filter_map f (multiset.filter p s) = multiset.filter_map (λ (x : α), ite (p x) (f x) none) s

@[simp]
theorem multiset.filter_map_some {α : Type u_1} (s : multiset α) :

@[simp]
theorem multiset.mem_filter_map {α : Type u_1} {β : Type u_2} (f : α → option β) (s : multiset α) {b : β} :
b multiset.filter_map f s ∃ (a : α), a s f a = some b

theorem multiset.map_filter_map_of_inv {α : Type u_1} {β : Type u_2} (f : α → option β) (g : β → α) (H : ∀ (x : α), option.map g (f x) = some x) (s : multiset α) :

theorem multiset.filter_map_le_filter_map {α : Type u_1} {β : Type u_2} (f : α → option β) {s t : multiset α} :

countp

def multiset.countp {α : Type u_1} (p : α → Prop) [decidable_pred p] :
multiset α

countp p s counts the number of elements of s (with multiplicity) that satisfy p.

Equations
@[simp]
theorem multiset.coe_countp {α : Type u_1} {p : α → Prop} [decidable_pred p] (l : list α) :

@[simp]
theorem multiset.countp_zero {α : Type u_1} (p : α → Prop) [decidable_pred p] :

@[simp]
theorem multiset.countp_cons_of_pos {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} (s : multiset α) :
p amultiset.countp p (a ::ₘ s) = multiset.countp p s + 1

@[simp]
theorem multiset.countp_cons_of_neg {α : Type u_1} {p : α → Prop} [decidable_pred p] {a : α} (s : multiset α) :

theorem multiset.countp_eq_card_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] (s : multiset α) :

@[simp]
theorem multiset.countp_add {α : Type u_1} {p : α → Prop} [decidable_pred p] (s t : multiset α) :

@[instance]
def multiset.countp.is_add_monoid_hom {α : Type u_1} {p : α → Prop} [decidable_pred p] :

theorem multiset.countp_pos {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : multiset α} :
0 < multiset.countp p s ∃ (a : α) (H : a s), p a

@[simp]
theorem multiset.countp_sub {α : Type u_1} {p : α → Prop} [decidable_pred p] [decidable_eq α] {s t : multiset α} :

theorem multiset.countp_pos_of_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] {s : multiset α} {a : α} :
a sp a0 < multiset.countp p s

theorem multiset.countp_le_of_le {α : Type u_1} {p : α → Prop} [decidable_pred p] {s t : multiset α} :

@[simp]
theorem multiset.countp_filter {α : Type u_1} {p : α → Prop} [decidable_pred p] {q : α → Prop} [decidable_pred q] (s : multiset α) :
multiset.countp p (multiset.filter q s) = multiset.countp (λ (a : α), p a q a) s

def multiset.count {α : Type u_1} [decidable_eq α] :
α → multiset α

count a s is the multiplicity of a in s.

Equations
@[simp]
theorem multiset.coe_count {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :

@[simp]
theorem multiset.count_zero {α : Type u_1} [decidable_eq α] (a : α) :

@[simp]
theorem multiset.count_cons_self {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

@[simp]
theorem multiset.count_cons_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (h : a b) (s : multiset α) :

theorem multiset.count_le_of_le {α : Type u_1} [decidable_eq α] (a : α) {s t : multiset α} :

theorem multiset.count_le_count_cons {α : Type u_1} [decidable_eq α] (a b : α) (s : multiset α) :

theorem multiset.count_cons {α : Type u_1} [decidable_eq α] (a b : α) (s : multiset α) :
multiset.count a (b ::ₘ s) = multiset.count a s + ite (a = b) 1 0

theorem multiset.count_singleton {α : Type u_1} [decidable_eq α] (a : α) :

@[simp]
theorem multiset.count_add {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

@[instance]

@[simp]
theorem multiset.count_smul {α : Type u_1} [decidable_eq α] (a : α) (n : ) (s : multiset α) :

theorem multiset.count_pos {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

@[simp]
theorem multiset.count_eq_zero_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a smultiset.count a s = 0

theorem multiset.count_eq_zero {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

theorem multiset.count_ne_zero {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

@[simp]
theorem multiset.count_repeat_self {α : Type u_1} [decidable_eq α] (a : α) (n : ) :

theorem multiset.count_repeat {α : Type u_1} [decidable_eq α] (a b : α) (n : ) :

@[simp]
theorem multiset.count_erase_self {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :

@[simp]
theorem multiset.count_erase_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (ab : a b) (s : multiset α) :

@[simp]
theorem multiset.count_sub {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

@[simp]
theorem multiset.count_union {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

@[simp]
theorem multiset.count_inter {α : Type u_1} [decidable_eq α] (a : α) (s t : multiset α) :

theorem multiset.count_sum {α : Type u_1} {β : Type u_2} [decidable_eq α] {m : multiset β} {f : β → multiset α} {a : α} :
multiset.count a (multiset.map f m).sum = (multiset.map (λ (b : β), multiset.count a (f b)) m).sum

theorem multiset.count_bind {α : Type u_1} {β : Type u_2} [decidable_eq α] {m : multiset β} {f : β → multiset α} {a : α} :
multiset.count a (m.bind f) = (multiset.map (λ (b : β), multiset.count a (f b)) m).sum

theorem multiset.le_count_iff_repeat_le {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} {n : } :

@[simp]
theorem multiset.count_filter_of_pos {α : Type u_1} [decidable_eq α] {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} :

@[simp]
theorem multiset.count_filter_of_neg {α : Type u_1} [decidable_eq α] {p : α → Prop} [decidable_pred p] {a : α} {s : multiset α} :

theorem multiset.ext {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s = t ∀ (a : α), multiset.count a s = multiset.count a t

@[ext]
theorem multiset.ext' {α : Type u_1} [decidable_eq α] {s t : multiset α} :
(∀ (a : α), multiset.count a s = multiset.count a t)s = t

@[simp]
theorem multiset.coe_inter {α : Type u_1} [decidable_eq α] (s t : list α) :

theorem multiset.le_iff_count {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s t ∀ (a : α), multiset.count a s multiset.count a t

inductive multiset.rel {α : Type u_1} {β : Type u_2} :
(α → β → Prop)multiset αmultiset β → Prop

rel r s t -- lift the relation r between two elements to a relation between s and t, s.t. there is a one-to-one mapping betweem elements in s and t following r.

theorem multiset.rel_flip {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : multiset β} {t : multiset α} :

theorem multiset.rel_eq_refl {α : Type u_1} {s : multiset α} :

theorem multiset.rel_eq {α : Type u_1} {s t : multiset α} :

theorem multiset.rel.mono {α : Type u_1} {β : Type u_2} {r p : α → β → Prop} {s : multiset α} {t : multiset β} :
(∀ (a : α) (b : β), r a bp a b)multiset.rel r s tmultiset.rel p s t

theorem multiset.rel.add {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : multiset α} {t : multiset β} {u : multiset α} {v : multiset β} :
multiset.rel r s tmultiset.rel r u vmultiset.rel r (s + u) (t + v)

theorem multiset.rel_flip_eq {α : Type u_1} {s t : multiset α} :
multiset.rel (λ (a b : α), b = a) s t s = t

@[simp]
theorem multiset.rel_zero_left {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {b : multiset β} :
multiset.rel r 0 b b = 0

@[simp]
theorem multiset.rel_zero_right {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : multiset α} :
multiset.rel r a 0 a = 0

theorem multiset.rel_cons_left {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {as : multiset α} {bs : multiset β} :
multiset.rel r (a ::ₘ as) bs ∃ (b : β) (bs' : multiset β), r a b multiset.rel r as bs' bs = b ::ₘ bs'

theorem multiset.rel_cons_right {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {as : multiset α} {b : β} {bs : multiset β} :
multiset.rel r as (b ::ₘ bs) ∃ (a : α) (as' : multiset α), r a b multiset.rel r as' bs as = a ::ₘ as'

theorem multiset.rel_add_left {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {as₀ as₁ : multiset α} {bs : multiset β} :
multiset.rel r (as₀ + as₁) bs ∃ (bs₀ bs₁ : multiset β), multiset.rel r as₀ bs₀ multiset.rel r as₁ bs₁ bs = bs₀ + bs₁

theorem multiset.rel_add_right {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {as : multiset α} {bs₀ bs₁ : multiset β} :
multiset.rel r as (bs₀ + bs₁) ∃ (as₀ as₁ : multiset α), multiset.rel r as₀ bs₀ multiset.rel r as₁ bs₁ as = as₀ + as₁

theorem multiset.rel_map_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {s : multiset γ} {f : γ → α} {t : multiset β} :
multiset.rel r (multiset.map f s) t multiset.rel (λ (a : γ) (b : β), r (f a) b) s t

theorem multiset.rel_map_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {s : multiset α} {t : multiset γ} {f : γ → β} :
multiset.rel r s (multiset.map f t) multiset.rel (λ (a : α) (b : γ), r a (f b)) s t

theorem multiset.rel_join {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : multiset (multiset α)} {t : multiset (multiset β)} :

theorem multiset.rel_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {p : γ → δ → Prop} {s : multiset α} {t : multiset β} {f : α → γ} {g : β → δ} :
(r p) f gmultiset.rel r s tmultiset.rel p (multiset.map f s) (multiset.map g t)

theorem multiset.rel_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {p : γ → δ → Prop} {s : multiset α} {t : multiset β} {f : α → multiset γ} {g : β → multiset δ} :
(r multiset.rel p) f gmultiset.rel r s tmultiset.rel p (s.bind f) (t.bind g)

theorem multiset.card_eq_card_of_rel {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : multiset α} {t : multiset β} :
multiset.rel r s ts.card = t.card

theorem multiset.exists_mem_of_rel_of_mem {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s : multiset α} {t : multiset β} (h : multiset.rel r s t) {a : α} :
a s(∃ (b : β) (H : b t), r a b)

theorem multiset.map_eq_map {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) {s t : multiset α} :

theorem multiset.map_injective {α : Type u_1} {β : Type u_2} {f : α → β} :

theorem multiset.map_mk_eq_map_mk_of_rel {α : Type u_1} {r : α → α → Prop} {s t : multiset α} :
multiset.rel r s tmultiset.map (quot.mk r) s = multiset.map (quot.mk r) t

theorem multiset.exists_multiset_eq_map_quot_mk {α : Type u_1} {r : α → α → Prop} (s : multiset (quot r)) :
∃ (t : multiset α), s = multiset.map (quot.mk r) t

theorem multiset.induction_on_multiset_quot {α : Type u_1} {r : α → α → Prop} {p : multiset (quot r) → Prop} (s : multiset (quot r)) :
(∀ (s : multiset α), p (multiset.map (quot.mk r) s))p s