# mathlib3documentation

data.multiset.basic

# Multisets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. These are implemented as the quotient of a list by permutations.

## Notation #

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

def multiset (α : Type u) :

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

Equations
Instances for `multiset`
@[protected, 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₂
@[protected, instance]
Equations
@[protected]
def multiset.sizeof {α : Type u_1} [has_sizeof α] (s : multiset α) :

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

Equations
• s.sizeof = multiset.sizeof._proof_1
@[protected, instance]
def multiset.has_sizeof {α : Type u_1} [has_sizeof α] :
Equations

### Empty multiset #

@[protected]
def multiset.zero {α : Type u_1} :

`0 : multiset α` is the empty set

Equations
@[protected, instance]
def multiset.has_zero {α : Type u_1} :
Equations
@[protected, instance]
def multiset.has_emptyc {α : Type u_1} :
Equations
@[protected, instance]
def multiset.inhabited_multiset {α : Type u_1} :
Equations
@[simp]
theorem multiset.coe_nil {α : Type u_1} :
@[simp]
theorem multiset.empty_eq_zero {α : Type u_1} :
= 0
@[simp]
theorem multiset.coe_eq_zero {α : Type u_1} (l : list α) :
l = 0
theorem multiset.coe_eq_zero_iff_empty {α : Type u_1} (l : list α) :
l = 0 (l.empty)

### `multiset.cons`#

def multiset.cons {α : Type u_1} (a : α) (s : multiset α) :

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

Equations
@[protected, instance]
def multiset.has_insert {α : Type u_1} :
(multiset α)
Equations
@[simp]
theorem multiset.insert_eq_cons {α : Type u_1} (a : α) (s : multiset α) :
= a ::ₘ s
@[simp]
theorem multiset.cons_coe {α : Type u_1} (a : α) (l : list α) :
a ::ₘ l = (a :: l)
@[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
@[protected]
theorem multiset.induction {α : Type u_1} {p : Prop} (h₁ : p 0) (h₂ : ⦃a : α⦄ {s : multiset α}, p s p (a ::ₘ s)) (s : multiset α) :
p s
@[protected]
theorem multiset.induction_on {α : Type u_1} {p : Prop} (s : multiset α) (h₁ : p 0) (h₂ : ⦃a : α⦄ {s : multiset α}, p s p (a ::ₘ s)) :
p s
theorem multiset.cons_swap {α : Type u_1} (a b : α) (s : multiset α) :
a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s
@[protected]
def multiset.rec {α : Type u_1} {C : Sort u_4} (C_0 : C 0) (C_cons : Π (a : α) (m : multiset α), C m C (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
@[protected]
def multiset.rec_on {α : Type u_1} {C : Sort u_4} (m : multiset α) (C_0 : C 0) (C_cons : Π (a : α) (m : multiset α), C m C (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)) :
C m

Companion to `multiset.rec` with more convenient argument order.

Equations
@[simp]
theorem multiset.rec_on_0 {α : Type u_1} {C : Sort u_4} {C_0 : C 0} {C_cons : Π (a : α) (m : multiset α), C m C (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 : Sort u_4} {C_0 : C 0} {C_cons : Π (a : α) (m : multiset α), C m C (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} (a : α) (s : multiset α) :
Prop

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

Equations
@[protected, instance]
def multiset.has_mem {α : Type u_1} :
(multiset α)
Equations
@[simp]
theorem multiset.mem_coe {α : Type u_1} {a : α} {l : list α} :
a l a l
@[protected, 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 α} (h : a s) :
a 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 ::ₘ s p x) p a (x : α), x s p 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)
theorem multiset.empty_or_exists_mem {α : 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

### Singleton #

@[protected, instance]
def multiset.has_singleton {α : Type u_1} :
(multiset α)
Equations
@[protected, instance]
@[simp]
theorem multiset.cons_zero {α : Type u_1} (a : α) :
a ::ₘ 0 = {a}
@[simp, norm_cast]
theorem multiset.coe_singleton {α : Type u_1} (a : α) :
[a] = {a}
@[simp]
theorem multiset.mem_singleton {α : Type u_1} {a b : α} :
b {a} b = a
theorem multiset.mem_singleton_self {α : Type u_1} (a : α) :
a {a}
@[simp]
theorem multiset.singleton_inj {α : Type u_1} {a b : α} :
{a} = {b} a = b
@[simp, norm_cast]
theorem multiset.coe_eq_singleton {α : Type u_1} {l : list α} {a : α} :
l = {a} l = [a]
@[simp]
theorem multiset.singleton_eq_cons_iff {α : Type u_1} {a b : α} (m : multiset α) :
{a} = b ::ₘ m a = b m = 0
theorem multiset.pair_comm {α : Type u_1} (x y : α) :
{x, y} = {y, x}

### `multiset.subset`#

@[protected]
def multiset.subset {α : Type u_1} (s t : 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
@[protected, instance]
def multiset.has_subset {α : Type u_1} :
Equations
@[protected, instance]
def multiset.has_ssubset {α : 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 t t u s u
theorem multiset.subset_iff {α : Type u_1} {s t : multiset α} :
s t ⦃x : α⦄, x s x t
theorem multiset.mem_of_subset {α : Type u_1} {s t : multiset α} {a : α} (h : s t) :
a s a t
@[simp]
theorem multiset.zero_subset {α : Type u_1} (s : multiset α) :
0 s
theorem multiset.subset_cons {α : Type u_1} (s : multiset α) (a : α) :
s a ::ₘ s
theorem multiset.ssubset_cons {α : Type u_1} {s : multiset α} {a : α} (ha : a s) :
s a ::ₘ s
@[simp]
theorem multiset.cons_subset {α : Type u_1} {a : α} {s t : multiset α} :
a ::ₘ s t a t s t
theorem multiset.cons_subset_cons {α : Type u_1} {a : α} {s t : multiset α} :
s t a ::ₘ s a ::ₘ t
theorem multiset.eq_zero_of_subset_zero {α : Type u_1} {s : multiset α} (h : s 0) :
s = 0
theorem multiset.subset_zero {α : Type u_1} {s : multiset α} :
s 0 s = 0
theorem multiset.induction_on' {α : Type u_1} {p : Prop} (S : multiset α) (h₁ : p 0) (h₂ : {a : α} {s : multiset α}, a S s S p s p s)) :
p S

### `multiset.to_list`#

noncomputable def multiset.to_list {α : Type u_1} (s : multiset α) :
list α

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

Equations
@[simp, norm_cast]
theorem multiset.coe_to_list {α : Type u_1} (s : multiset α) :
@[simp]
theorem multiset.to_list_eq_nil {α : Type u_1} {s : multiset α} :
s = 0
@[simp]
theorem multiset.empty_to_list {α : Type u_1} {s : multiset α} :
@[simp]
theorem multiset.to_list_zero {α : Type u_1} :
@[simp]
theorem multiset.mem_to_list {α : Type u_1} {a : α} {s : multiset α} :
a s.to_list a s
@[simp]
theorem multiset.to_list_eq_singleton_iff {α : Type u_1} {a : α} {m : multiset α} :
m.to_list = [a] m = {a}
@[simp]
theorem multiset.to_list_singleton {α : Type u_1} (a : α) :
{a}.to_list = [a]

### Partial order on `multiset`s #

@[protected]
def multiset.le {α : Type u_1} (s t : 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
• s.le t = multiset.le._proof_1
@[protected, instance]
def multiset.partial_order {α : Type u_1} :
Equations
@[protected, instance]
def multiset.decidable_le {α : Type u_1} [decidable_eq α] :
Equations
theorem multiset.subset_of_le {α : Type u_1} {s t : multiset α} :
s t s t
theorem multiset.le.subset {α : Type u_1} {s t : multiset α} :
s t s t

Alias of `multiset.subset_of_le`.

theorem multiset.mem_of_le {α : Type u_1} {s t : multiset α} {a : α} (h : s t) :
a s a t
theorem multiset.not_mem_mono {α : Type u_1} {s t : multiset α} {a : α} (h : s t) :
a t a s
@[simp]
theorem multiset.coe_le {α : Type u_1} {l₁ l₂ : list α} :
l₁ l₂ l₁ <+~ l₂
theorem multiset.le_induction_on {α : Type u_1} {C : Prop} {s t : multiset α} (h : s t) (H : {l₁ l₂ : list α}, l₁ <+ l₂ C l₁ l₂) :
C s t
theorem multiset.zero_le {α : Type u_1} (s : multiset α) :
0 s
@[protected, instance]
def multiset.order_bot {α : Type u_1} :
Equations
@[simp]
theorem multiset.bot_eq_zero {α : Type u_1} :
= 0

This is a `rfl` and `simp` version of `bot_eq_zero`.

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} {s t : multiset α} (a : α) :
a ::ₘ s a ::ₘ t s t
theorem multiset.cons_le_cons {α : Type u_1} {s t : multiset α} (a : α) :
s t a ::ₘ s a ::ₘ t
theorem multiset.le_cons_of_not_mem {α : Type u_1} {s t : multiset α} {a : α} (m : a s) :
s a ::ₘ t s t
@[simp]
theorem multiset.singleton_ne_zero {α : Type u_1} (a : α) :
{a} 0
@[simp]
theorem multiset.singleton_le {α : Type u_1} {a : α} {s : multiset α} :
{a} s a s

@[protected]
def multiset.add {α : Type u_1} (s₁ s₂ : 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
• s₁.add s₂ = s₂ (λ (l₁ l₂ : list α), (l₁ ++ l₂)) multiset.add._proof_1
@[protected, instance]
def multiset.has_add {α : Type u_1} :
Equations
@[simp]
theorem multiset.coe_add {α : Type u_1} (s t : list α) :
s + t = (s ++ t)
@[simp]
theorem multiset.singleton_add {α : Type u_1} (a : α) (s : multiset α) :
{a} + s = a ::ₘ s
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
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
theorem multiset.le_iff_exists_add {α : Type u_1} {s t : multiset α} :
s t (u : multiset α), t = s + u
@[protected, instance]
Equations
@[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)
@[simp]
theorem multiset.mem_add {α : Type u_1} {a : α} {s t : multiset α} :
a s + t a s a t
theorem multiset.mem_of_mem_nsmul {α : Type u_1} {a : α} {s : multiset α} {n : } (h : a n s) :
a s
@[simp]
theorem multiset.mem_nsmul {α : Type u_1} {a : α} {s : multiset α} {n : } (h0 : n 0) :
a n s a s
theorem multiset.nsmul_cons {α : Type u_1} {s : multiset α} (n : ) (a : α) :
n (a ::ₘ s) = n {a} + n s

### Cardinality #

def multiset.card {α : Type u_1} :

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.length_to_list {α : Type u_1} (s : multiset α) :
@[simp]
theorem multiset.card_zero {α : Type u_1} :
theorem multiset.card_add {α : Type u_1} (s t : multiset α) :
theorem multiset.card_nsmul {α : Type u_1} (s : multiset α) (n : ) :
@[simp]
theorem multiset.card_cons {α : Type u_1} (a : α) (s : multiset α) :
@[simp]
theorem multiset.card_singleton {α : Type u_1} (a : α) :
= 1
theorem multiset.card_pair {α : Type u_1} (a b : α) :
theorem multiset.card_eq_one {α : Type u_1} {s : multiset α} :
(a : α), s = {a}
theorem multiset.card_le_of_le {α : Type u_1} {s t : multiset α} (h : s t) :
theorem multiset.card_mono {α : Type u_1} :
theorem multiset.eq_of_le_of_card_le {α : Type u_1} {s t : multiset α} (h : s t) :
s = t
theorem multiset.card_lt_of_lt {α : Type u_1} {s t : multiset α} (h : s < t) :
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 = 0
theorem multiset.card_pos {α : Type u_1} {s : multiset α} :
s 0
theorem multiset.card_pos_iff_exists_mem {α : Type u_1} {s : multiset α} :
(a : α), a s
theorem multiset.card_eq_two {α : Type u_1} {s : multiset α} :
(x y : α), s = {x, y}
theorem multiset.card_eq_three {α : Type u_1} {s : multiset α} :
(x y z : α), s = {x, y, z}

### Induction principles #

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

A strong induction principle for multisets: If you construct a value for a particular multiset given values for all strictly smaller multisets, you can construct a value for any multiset.

Equations
theorem multiset.strong_induction_eq {α : Type u_1} {p : Sort u_2} (s : multiset α) (H : Π (s : multiset α), (Π (t : multiset α), t < s p t) p s) :
= H s (λ (t : multiset α) (h : t < s),
theorem multiset.case_strong_induction_on {α : Type u_1} {p : Prop} (s : multiset α) (h₀ : p 0) (h₁ : (a : α) (s : multiset α), ( (t : multiset α), t s p t) p (a ::ₘ s)) :
p s
def multiset.strong_downward_induction {α : Type u_1} {p : Sort u_2} {n : } (H : Π (t₁ : multiset α), (Π {t₂ : multiset α}, n t₁ < t₂ p t₂) n p t₁) (s : multiset α) :
p s

Suppose that, given that `p t` can be defined on all supersets of `s` of cardinality less than `n`, one knows how to define `p s`. Then one can inductively define `p s` for all multisets `s` of cardinality less than `n`, starting from multisets of card `n` and iterating. This can be used either to define data, or to prove properties.

Equations
theorem multiset.strong_downward_induction_eq {α : Type u_1} {p : Sort u_2} {n : } (H : Π (t₁ : multiset α), (Π {t₂ : multiset α}, n t₁ < t₂ p t₂) n p t₁) (s : multiset α) :
= H s (λ (t : multiset α) (ht : n) (hst : s < t),
def multiset.strong_downward_induction_on {α : Type u_1} {p : Sort u_2} {n : } (s : multiset α) :
(Π (t₁ : multiset α), (Π {t₂ : multiset α}, n t₁ < t₂ p t₂) n p t₁) p s

Analogue of `strong_downward_induction` with order of arguments swapped.

Equations
theorem multiset.strong_downward_induction_on_eq {α : Type u_1} {p : Sort u_2} (s : multiset α) {n : } (H : Π (t₁ : multiset α), (Π {t₂ : multiset α}, n t₁ < t₂ p t₂) n p t₁) :
= H s (λ (t : multiset α) (ht : n) (h : s < t), ht)
theorem multiset.well_founded_lt {α : Type u_1} :

Another way of expressing `strong_induction_on`: the `(<)` relation is well-founded.

@[protected, instance]
def multiset.is_well_founded_lt {α : Type u_1} :

### `multiset.replicate`#

def multiset.replicate {α : Type u_1} (n : ) (a : α) :

`replicate n a` is the multiset containing only `a` with multiplicity `n`.

Equations
theorem multiset.coe_replicate {α : Type u_1} (n : ) (a : α) :
a) =
@[simp]
theorem multiset.replicate_zero {α : Type u_1} (a : α) :
= 0
@[simp]
theorem multiset.replicate_succ {α : Type u_1} (a : α) (n : ) :
theorem multiset.replicate_add {α : Type u_1} (m n : ) (a : α) :
def multiset.replicate_add_monoid_hom {α : Type u_1} (a : α) :

`multiset.replicate` as an `add_monoid_hom`.

Equations
@[simp]
theorem multiset.replicate_add_monoid_hom_apply {α : Type u_1} (a : α) (n : ) :
theorem multiset.replicate_one {α : Type u_1} (a : α) :
= {a}
@[simp]
theorem multiset.card_replicate {α : Type u_1} (n : ) (a : α) :
theorem multiset.mem_replicate {α : Type u_1} {a b : α} {n : } :
b n 0 b = a
theorem multiset.eq_of_mem_replicate {α : Type u_1} {a b : α} {n : } :
b b = a
theorem multiset.eq_replicate_card {α : Type u_1} {a : α} {s : multiset α} :
(b : α), b s b = a
theorem multiset.eq_replicate_of_mem {α : Type u_1} {a : α} {s : multiset α} :
( (b : α), b s b = a)

Alias of the reverse direction of `multiset.eq_replicate_card`.

theorem multiset.eq_replicate {α : Type u_1} {a : α} {n : } {s : multiset α} :
s = (b : α), b s b = a
theorem multiset.replicate_right_injective {α : Type u_1} {n : } (hn : n 0) :
@[simp]
theorem multiset.replicate_right_inj {α : Type u_1} {a b : α} {n : } (h : n 0) :
a = b
theorem multiset.replicate_left_injective {α : Type u_1} (a : α) :
theorem multiset.replicate_subset_singleton {α : Type u_1} (n : ) (a : α) :
{a}
theorem multiset.replicate_le_coe {α : Type u_1} {a : α} {n : } {l : list α} :
theorem multiset.nsmul_singleton {α : Type u_1} (a : α) (n : ) :
n {a} =
theorem multiset.nsmul_replicate {α : Type u_1} {a : α} (n m : ) :
theorem multiset.replicate_le_replicate {α : Type u_1} (a : α) {k n : } :
k n
theorem multiset.le_replicate_iff {α : Type u_1} {m : multiset α} {a : α} {n : } :
m (k : ) (H : k n), m =
theorem multiset.lt_replicate_succ {α : Type u_1} {m : multiset α} {x : α} {n : } :

### Erasing one copy of an element #

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

`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 α) (h : b a) :
(b ::ₘ s).erase a = b ::ₘ s.erase a
@[simp]
theorem multiset.erase_singleton {α : Type u_1} [decidable_eq α] (a : α) :
{a}.erase a = 0
@[simp]
theorem multiset.erase_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a s s.erase a = s
@[simp]
theorem multiset.cons_erase {α : Type u_1} [decidable_eq α] {s : multiset α} {a : α} :
a s a ::ₘ s.erase a = s
theorem multiset.le_cons_erase {α : Type u_1} [decidable_eq α] (s : multiset α) (a : α) :
s a ::ₘ s.erase a
theorem multiset.add_singleton_eq_iff {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :
s + {a} = t a t s = t.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 α} (h : 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 α} (h : 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 α} (ab : 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 b a 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 : α) (h : s t) :
s.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 α} :
@[simp]
theorem multiset.card_erase_add_one {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
theorem multiset.card_erase_lt_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
theorem multiset.card_erase_le {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
theorem multiset.card_erase_eq_ite {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
@[simp]
theorem multiset.coe_reverse {α : Type u_1} (l : list α) :

### `multiset.map`#

def multiset.map {α : Type u_1} {β : Type u_2} (f : α β) (s : 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
Instances for `multiset.map`
theorem multiset.map_congr {α : Type u_1} {β : Type u_2} {f g : α β} {s t : multiset α} :
s = t ( (x : α), x t f x = g x) s = t
theorem multiset.map_hcongr {α : Type u_1} {β β' : Type u_2} {m : multiset α} {f : α β} {f' : α β'} (h : β = β') (hf : (a : α), a m f a == f' a) :
m == m
theorem multiset.forall_mem_map_iff {α : Type u_1} {β : Type u_2} {f : α β} {p : β Prop} {s : multiset α} :
( (y : β), y s p y) (x : α), x s p (f x)
@[simp]
theorem multiset.coe_map {α : Type u_1} {β : Type u_2} (f : α β) (l : list α) :
= (list.map f l)
@[simp]
theorem multiset.map_zero {α : Type u_1} {β : Type u_2} (f : α β) :
0 = 0
@[simp]
theorem multiset.map_cons {α : Type u_1} {β : Type u_2} (f : α β) (a : α) (s : multiset α) :
(a ::ₘ s) = f a ::ₘ s
theorem multiset.map_comp_cons {α : Type u_1} {β : Type u_2} (f : α β) (t : α) :
@[simp]
theorem multiset.map_singleton {α : Type u_1} {β : Type u_2} (f : α β) (a : α) :
{a} = {f a}
@[simp]
theorem multiset.map_replicate {α : Type u_1} {β : Type u_2} (f : α β) (a : α) (k : ) :
a) = (f a)
@[simp]
theorem multiset.map_add {α : Type u_1} {β : Type u_2} (f : α β) (s t : multiset α) :
(s + t) = s + t
@[protected, instance]
def multiset.can_lift {α : Type u_1} {β : Type u_2} (c : out_param α)) (p : out_param Prop)) [ β c p] :
can_lift (multiset α) (multiset β) (multiset.map c) (λ (s : multiset α), (x : α), x s p x)

If each element of `s : multiset α` can be lifted to `β`, then `s` can be lifted to `multiset β`.

Equations
def multiset.map_add_monoid_hom {α : Type u_1} {β : Type u_2} (f : α β) :

`multiset.map` as an `add_monoid_hom`.

Equations
@[simp]
theorem multiset.coe_map_add_monoid_hom {α : Type u_1} {β : Type u_2} (f : α β) :
theorem multiset.map_nsmul {α : Type u_1} {β : Type u_2} (f : α β) (n : ) (s : multiset α) :
(n s) = n s
@[simp]
theorem multiset.mem_map {α : Type u_1} {β : Type u_2} {f : α β} {b : β} {s : multiset α} :
b 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 : α β} :
s = 0 s = 0
theorem multiset.mem_map_of_mem {α : Type u_1} {β : Type u_2} (f : α β) {a : α} {s : multiset α} (h : a s) :
f a s
theorem multiset.map_eq_singleton {α : Type u_1} {β : Type u_2} {f : α β} {s : multiset α} {b : β} :
s = {b} (a : α), s = {a} f a = b
theorem multiset.map_eq_cons {α : Type u_1} {β : Type u_2} [decidable_eq α] (f : α β) (s : multiset α) (t : multiset β) (b : β) :
( (a : α) (H : a s), f a = b (s.erase a) = t) s = b ::ₘ t
theorem multiset.mem_map_of_injective {α : Type u_1} {β : Type u_2} {f : α β} (H : function.injective f) {a : α} {s : multiset α} :
f a s a s
@[simp]
theorem multiset.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β γ) (f : α β) (s : multiset α) :
s) = multiset.map (g f) s
theorem multiset.map_id {α : Type u_1} (s : multiset α) :
= s
@[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 : β) :
s =
theorem multiset.map_const' {α : Type u_1} {β : Type u_2} (s : multiset α) (b : β) :
multiset.map (λ (_x : α), b) s =
theorem multiset.eq_of_mem_map_const {α : Type u_1} {β : Type u_2} {b₁ b₂ : β} {l : list α} (h : b₁ multiset.map b₂) l) :
b₁ = b₂
@[simp]
theorem multiset.map_le_map {α : Type u_1} {β : Type u_2} {f : α β} {s t : multiset α} (h : s t) :
s t
@[simp]
theorem multiset.map_lt_map {α : Type u_1} {β : Type u_2} {f : α β} {s t : multiset α} (h : s < t) :
s < t
theorem multiset.map_mono {α : Type u_1} {β : Type u_2} (f : α β) :
theorem multiset.map_strict_mono {α : Type u_1} {β : Type u_2} (f : α β) :
@[simp]
theorem multiset.map_subset_map {α : Type u_1} {β : Type u_2} {f : α β} {s t : multiset α} (H : s t) :
s t
theorem multiset.map_erase {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α β) (hf : function.injective f) (x : α) (s : multiset α) :
(s.erase x) = s).erase (f x)
theorem multiset.map_surjective_of_surjective {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.surjective f) :

### `multiset.fold`#

def multiset.foldl {α : Type u_1} {β : Type u_2} (f : β α β) (H : right_commutative f) (b : β) (s : 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
• b s = (λ (l : list α), b l) _
@[simp]
theorem multiset.foldl_zero {α : Type u_1} {β : Type u_2} (f : β α β) (H : right_commutative f) (b : β) :
b 0 = b
@[simp]
theorem multiset.foldl_cons {α : Type u_1} {β : Type u_2} (f : β α β) (H : right_commutative f) (b : β) (a : α) (s : multiset α) :
b (a ::ₘ s) = (f b a) s
@[simp]
theorem multiset.foldl_add {α : Type u_1} {β : Type u_2} (f : β α β) (H : right_commutative f) (b : β) (s t : multiset α) :
b (s + t) = H b s) t
def multiset.foldr {α : Type u_1} {β : Type u_2} (f : α β β) (H : left_commutative f) (b : β) (s : 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
• b s = (λ (l : list α), b l) _
@[simp]
theorem multiset.foldr_zero {α : Type u_1} {β : Type u_2} (f : α β β) (H : left_commutative f) (b : β) :
b 0 = b
@[simp]
theorem multiset.foldr_cons {α : Type u_1} {β : Type u_2} (f : α β β) (H : left_commutative f) (b : β) (a : α) (s : multiset α) :
b (a ::ₘ s) = f a H b s)
@[simp]
theorem multiset.foldr_singleton {α : Type u_1} {β : Type u_2} (f : α β β) (H : left_commutative f) (b : β) (a : α) :
b {a} = f a b
@[simp]
theorem multiset.foldr_add {α : Type u_1} {β : Type u_2} (f : α β β) (H : left_commutative f) (b : β) (s t : multiset α) :
b (s + t) = H b t) s
@[simp]
theorem multiset.coe_foldr {α : Type u_1} {β : Type u_2} (f : α β β) (H : left_commutative f) (b : β) (l : list α) :
b l = b l
@[simp]
theorem multiset.coe_foldl {α : Type u_1} {β : Type u_2} (f : β α β) (H : right_commutative f) (b : β) (l : list α) :
b l = b l
theorem multiset.coe_foldr_swap {α : Type u_1} {β : Type u_2} (f : α β β) (H : left_commutative f) (b : β) (l : list α) :
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 α) :
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 α) :
b s = multiset.foldr (λ (x : α) (y : β), f y x) _ b s
theorem multiset.foldr_induction' {α : Type u_1} {β : Type u_2} (f : α β β) (H : left_commutative f) (x : β) (q : α Prop) (p : β Prop) (s : multiset α) (hpqf : (a : α) (b : β), q a p b p (f a b)) (px : p x) (q_s : (a : α), a s q a) :
p H x s)
theorem multiset.foldr_induction {α : Type u_1} (f : α α α) (H : left_commutative f) (x : α) (p : α Prop) (s : multiset α) (p_f : (a b : α), p a p b p (f a b)) (px : p x) (p_s : (a : α), a s p a) :
p H x s)
theorem multiset.foldl_induction' {α : Type u_1} {β : Type u_2} (f : β α β) (H : right_commutative f) (x : β) (q : α Prop) (p : β Prop) (s : multiset α) (hpqf : (a : α) (b : β), q a p b p (f b a)) (px : p x) (q_s : (a : α), a s q a) :
p H x s)
theorem multiset.foldl_induction {α : Type u_1} (f : α α α) (H : right_commutative f) (x : α) (p : α Prop) (s : multiset α) (p_f : (a b : α), p a p b p (f b a)) (px : p x) (p_s : (a : α), a s p a) :
p H x s)

### Map for partial functions #

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

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 l p a) :
H = l H)
@[simp]
theorem multiset.pmap_zero {α : Type u_1} {β : Type u_2} {p : α Prop} (f : Π (a : α), p a β) (h : (a : α), a 0 p a) :
h = 0
@[simp]
theorem multiset.pmap_cons {α : Type u_1} {β : Type u_2} {p : α Prop} (f : Π (a : α), p a β) (a : α) (m : multiset α) (h : (b : α), b a ::ₘ m p b) :
(a ::ₘ m) h = f a _ ::ₘ _
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 α} (hx : x s) :
<
theorem multiset.pmap_eq_map {α : Type u_1} {β : Type u_2} (p : α Prop) (f : α β) (s : multiset α) (H : (a : α), a s p a) :
multiset.pmap (λ (a : α) (_x : p a), f a) s H = 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 s p a} {H₂ : (a : α), a s q a} :
( (a : α), a s (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) H₁ = 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 s p a) :
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 s p a) :
H = multiset.map (λ (x : {x // x s}), f x _) s.attach
@[simp]
theorem multiset.attach_map_coe' {α : Type u_1} {β : Type u_2} (s : multiset α) (f : α β) :
multiset.map (λ (i : {x // x s}), f i) s.attach = s
theorem multiset.attach_map_val' {α : Type u_1} {β : Type u_2} (s : multiset α) (f : α β) :
multiset.map (λ (i : {x // x s}), f i.val) s.attach = s
@[simp]
theorem multiset.attach_map_coe {α : Type u_1} (s : multiset α) :
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 s p a} {b : β} :
b 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 s p 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
@[protected]
def multiset.decidable_forall_multiset {α : Type u_1} {m : multiset α} {p : α Prop} [hp : Π (a : α), decidable (p a)] :
decidable ( (a : α), a m p a)

If `p` is a decidable predicate, so is the predicate that all elements of a multiset satisfy `p`.

Equations
@[protected, 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
@[protected, 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
@[protected]
def multiset.decidable_exists_multiset {α : Type u_1} {m : multiset α} {p : α Prop}  :
decidable ( (x : α) (H : x m), p x)

If `p` is a decidable predicate, so is the existence of an element in a multiset satisfying `p`.

Equations
@[protected, 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

### Subtraction #

@[protected]
def multiset.sub {α : Type u_1} [decidable_eq α] (s t : multiset α) :

`s - t` is the multiset such that `count a (s - t) = count a s - count a t` for all `a` (note that it is truncated subtraction, so it is `0` if `count a t ≥ count a s`).

Equations
• s.sub t = (λ (l₁ l₂ : list α), (l₁.diff l₂)) multiset.sub._proof_1
@[protected, 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)
@[protected]
theorem multiset.sub_zero {α : Type u_1} [decidable_eq α] (s : multiset α) :
s - 0 = s

This is a special case of `tsub_zero`, which should be used instead of this. This is needed to prove `has_ordered_sub (multiset α)`.

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

This is a special case of `tsub_le_iff_right`, which should be used instead of this. This is needed to prove `has_ordered_sub (multiset α)`.

@[protected, instance]
def multiset.has_ordered_sub {α : Type u_1} [decidable_eq α] :
theorem multiset.cons_sub_of_le {α : Type u_1} [decidable_eq α] (a : α) {s t : multiset α} (h : t s) :
a ::ₘ s - t = a ::ₘ (s - t)
theorem multiset.sub_eq_fold_erase {α : Type u_1} [decidable_eq α] (s t : multiset α) :
@[simp]
theorem multiset.card_sub {α : Type u_1} [decidable_eq α] {s t : multiset α} (h : t s) :

### Union #

def multiset.union {α : Type u_1} [decidable_eq α] (s t : 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
@[protected, 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 s s 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 α} (h₁ : s u) (h₂ : t u) :
s 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 α} :
(s t) = s t

### Intersection #

def multiset.inter {α : Type u_1} [decidable_eq α] (s t : 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
@[protected, 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 α} (h₁ : s t) (h₂ : s u) :
s t u
@[simp]
theorem multiset.mem_inter {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :
a s t a s a t
@[protected, instance]
def multiset.lattice {α : Type u_1} [decidable_eq α] :
Equations
@[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 α} (h : s t) :
s 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

### `multiset.filter`#

def multiset.filter {α : Type u_1} (p : α Prop) (s : 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) (l : list α) :
= l)
@[simp]
theorem multiset.filter_zero {α : Type u_1} (p : α Prop)  :
= 0
theorem multiset.filter_congr {α : Type u_1} {p q : α Prop} {s : multiset α} :
( (x : α), x s (p x q x)) =
@[simp]
theorem multiset.filter_add {α : Type u_1} (p : α Prop) (s t : multiset α) :
(s + t) = +
@[simp]
theorem multiset.filter_le {α : Type u_1} (p : α Prop) (s : multiset α) :
s
@[simp]
theorem multiset.filter_subset {α : Type u_1} (p : α Prop) (s : multiset α) :
s
theorem multiset.filter_le_filter {α : Type u_1} (p : α Prop) {s t : multiset α} (h : s t) :
theorem multiset.monotone_filter_left {α : Type u_1} (p : α Prop)  :
theorem multiset.monotone_filter_right {α : Type u_1} (s : multiset α) ⦃p q : α Prop⦄ (h : p q) :
@[simp]
theorem multiset.filter_cons_of_pos {α : Type u_1} {p : α Prop} {a : α} (s : multiset α) :
p a (a ::ₘ s) = a ::ₘ
@[simp]
theorem multiset.filter_cons_of_neg {α : Type u_1} {p : α Prop} {a : α} (s : multiset α) :
¬p a (a ::ₘ s) =
@[simp]
theorem multiset.mem_filter {α : Type u_1} {p : α Prop} {a : α} {s : multiset α} :
a a s p a
theorem multiset.of_mem_filter {α : Type u_1} {p : α Prop} {a : α} {s : multiset α} (h : a ) :
p a
theorem multiset.mem_of_mem_filter {α : Type u_1} {p : α Prop} {a : α} {s : multiset α} (h : a ) :
a s
theorem multiset.mem_filter_of_mem {α : Type u_1} {p : α Prop} {a : α} {l : multiset α} (m : a l) (h : p a) :
a
theorem multiset.filter_eq_self {α : Type u_1} {p : α Prop} {s : multiset α} :
= s (a : α), a s p a
theorem multiset.filter_eq_nil {α : Type u_1} {p : α Prop} {s : multiset α} :
= 0 (a : α), a s ¬p a
theorem multiset.le_filter {α : Type u_1} {p : α Prop} {s t : multiset α} :
s s t (a : α), a s p a
theorem multiset.filter_cons {α : Type u_1} {p : α Prop} {a : α} (s : multiset α) :
(a ::ₘ s) = ite (p a) {a} 0 +
theorem multiset.filter_singleton {α : Type u_1} {a : α} (p : α Prop)  :
{a} = ite (p a) {a}
theorem multiset.filter_nsmul {α : Type u_1} {p : α Prop} (s : multiset α) (n : ) :
(n s) = n
@[simp]
theorem multiset.filter_sub {α : Type u_1} (p : α Prop) [decidable_eq α] (s t : multiset α) :
(s - t) = -
@[simp]
theorem multiset.filter_union {α : Type u_1} (p : α Prop) [decidable_eq α] (s t : multiset α) :
(s t) =
@[simp]
theorem multiset.filter_inter {α : Type u_1} (p : α Prop) [decidable_eq α] (s t : multiset α) :
(s t) =
@[simp]
theorem multiset.filter_filter {α : Type u_1} (p : α Prop) (q : α Prop) (s : multiset α) :
s) = multiset.filter (λ (a : α), p a q a) s
theorem multiset.filter_comm {α : Type u_1} (p : α Prop) (q : α Prop) (s : multiset α) :
s) = s)
theorem multiset.filter_add_filter {α : Type u_1} (p : α Prop) (q : α Prop) (s : multiset α) :
+ = 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) (s : multiset α) :
+ multiset.filter (λ (a : α), ¬p a) s = s
theorem multiset.map_filter {α : Type u_1} {β : Type u_2} (p : α Prop) (f : β α) (s : multiset β) :
s) = (multiset.filter (p f) s)
theorem multiset.map_filter' {α : Type u_1} {β : Type u_2} (p : α Prop) {f : α β} (hf : function.injective f) (s : multiset α) [decidable_pred (λ (b : β), (a : α), p a f a = b)] :
s) = multiset.filter (λ (b : β), (a : α), p a f a = b) s)

### Simultaneously filter and map elements of a multiset #

def multiset.filter_map {α : Type u_1} {β : Type u_2} (f : α ) (s : 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 : α ) (l : list α) :
= l)
@[simp]
theorem multiset.filter_map_zero {α : Type u_1} {β : Type u_2} (f : α ) :
= 0
@[simp]
theorem multiset.filter_map_cons_none {α : Type u_1} {β : Type u_2} {f : α } (a : α) (s : multiset α) (h : f a = option.none) :
(a ::ₘ s) =
@[simp]
theorem multiset.filter_map_cons_some {α : Type u_1} {β : Type u_2} (f : α ) (a : α) (s : multiset α) {b : β} (h : f a = ) :
(a ::ₘ s) =
theorem multiset.filter_map_eq_map {α : Type u_1} {β : Type u_2} (f : α β) :
theorem multiset.filter_map_eq_filter {α : Type u_1} (p : α Prop)  :
theorem multiset.filter_map_filter_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ) (g : β ) (s : multiset α) :
= multiset.filter_map (λ (x : α), (f x).bind g) s
theorem multiset.map_filter_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ) (g : β γ) (s : multiset α) :
s) = multiset.filter_map (λ (x : α), (f x)) s
theorem multiset.filter_map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : β ) (s : multiset α) :
theorem multiset.filter_filter_map {α : Type u_1} {β : Type u_2} (f : α ) (p : β Prop) (s : multiset α) :
= multiset.filter_map (λ (x : α), (f x)) s
theorem multiset.filter_map_filter {α : Type u_1} {β : Type u_2} (p : α Prop) (f : α ) (s : multiset α) :
= multiset.filter_map (λ (x : α), ite (p x) (f x) option.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 : α ) (s : multiset α) {b : β} :
b (a : α), a s f a =
theorem multiset.map_filter_map_of_inv {α : Type u_1} {β : Type u_2} (f : α ) (g : β α) (H : (x : α), (f x) = ) (s : multiset α) :
s) = s
theorem multiset.filter_map_le_filter_map {α : Type u_1} {β : Type u_2} (f : α ) {s t : multiset α} (h : s t) :

### countp #

def multiset.countp {α : Type u_1} (p : α Prop) (s : 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) (l : list α) :
= l
@[simp]
theorem multiset.countp_zero {α : Type u_1} (p : α Prop)  :
= 0
@[simp]
theorem multiset.countp_cons_of_pos {α : Type u_1} {p : α Prop} {a : α} (s : multiset α) :
p a (a ::ₘ s) = + 1
@[simp]
theorem multiset.countp_cons_of_neg {α : Type u_1} {p : α Prop} {a : α} (s : multiset α) :
¬p a (a ::ₘ s) =
theorem multiset.countp_cons {α : Type u_1} (p : α Prop) (b : α) (s : multiset α) :
(b ::ₘ s) = + ite (p b) 1 0
theorem multiset.countp_eq_card_filter {α : Type u_1} (p : α Prop) (s : multiset α) :
theorem multiset.countp_le_card {α : Type u_1} (p : α Prop) (s : multiset α) :
@[simp]
theorem multiset.countp_add {α : Type u_1} (p : α Prop) (s t : multiset α) :
(s + t) = +
@[simp]
theorem multiset.countp_nsmul {α : Type u_1} (p : α Prop) (s : multiset α) (n : ) :
(n s) = n *
theorem multiset.card_eq_countp_add_countp {α : Type u_1} (p : α Prop) (s : multiset α) :
= + multiset.countp (λ (x : α), ¬p x) s
def multiset.countp_add_monoid_hom {α : Type u_1} (p : α Prop)  :

`countp p`, the number of elements of a multiset satisfying `p`, promoted to an `add_monoid_hom`.

Equations
@[simp]
theorem multiset.coe_countp_add_monoid_hom {α : Type u_1} (p : α Prop)  :
@[simp]
theorem multiset.countp_sub {α : Type u_1} (p : α Prop) [decidable_eq α] {s t : multiset α} (h : t s) :
(s - t) = -
theorem multiset.countp_le_of_le {α : Type u_1} (p : α Prop) {s t : multiset α} (h : s t) :
@[simp]
theorem multiset.countp_filter {α : Type u_1} (p : α Prop) (q : α Prop) (s : multiset α) :
s) = multiset.countp (λ (a : α), p a q a) s
theorem multiset.countp_eq_countp_filter_add {α : Type u_1} (s : multiset α) (p q : α Prop)  :
= s) + (multiset.filter (λ (a : α), ¬q a) s)
@[simp]
theorem multiset.countp_true {α : Type u_1} {s : multiset α} :
multiset.countp (λ (_x : α), true) s =
@[simp]
theorem multiset.countp_false {α : Type u_1} {s : multiset α} :
multiset.countp (λ (_x : α), false) s = 0
theorem multiset.countp_map {α : Type u_1} {β : Type u_2} (f : α β) (s : multiset α) (p : β Prop)  :
s) = multiset.card (multiset.filter (λ (a : α), p (f a)) s)
@[simp]
theorem multiset.countp_attach {α : Type u_1} (p : α Prop) (s : multiset α) :
multiset.countp (λ (a : {x // x s}), p a) s.attach =
@[simp]
theorem multiset.filter_attach {α : Type u_1} (m : multiset α) (p : α Prop)  :
multiset.filter (λ (x : {x // x m}), p x) m.attach = m).attach
theorem multiset.countp_pos {α : Type u_1} {p : α Prop} {s : multiset α} :
0 < (a : α) (H : a s), p a
theorem multiset.countp_eq_zero {α : Type u_1} {p : α Prop} {s : multiset α} :
= 0 (a : α), a s ¬p a
theorem multiset.countp_eq_card {α : Type u_1} {p : α Prop} {s : multiset α} :
(a : α), a s p a
theorem multiset.countp_pos_of_mem {α : Type u_1} {p : α Prop} {s : multiset α} {a : α} (h : a s) (pa : p a) :
0 <
theorem multiset.countp_congr {α : Type u_1} {s s' : multiset α} (hs : s = s') {p p' : α Prop} [decidable_pred p'] (hp : (x : α), x s (p x p' x)) :
= s'

### Multiplicity of an element #

def multiset.count {α : Type u_1} [decidable_eq α] (a : α) :

`count a s` is the multiplicity of `a` in `s`.

Equations
@[simp]
theorem multiset.coe_count {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
= l
@[simp]
theorem multiset.count_zero {α : Type u_1} [decidable_eq α] (a : α) :
= 0
@[simp]
theorem multiset.count_cons_self {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :
(a ::ₘ s) = s).succ
@[simp]
theorem multiset.count_cons_of_ne {α : Type u_1} [decidable_eq α] {a b : α} (h : a b) (s : multiset α) :
(b ::ₘ s) =
theorem multiset.count_le_card {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :
theorem multiset.count_le_of_le {α : Type u_1} [decidable_eq α] (a : α) {s t : multiset α} :
s t
theorem multiset.count_le_count_cons {α : Type u_1} [decidable_eq α] (a b : α) (s : multiset α) :
(b ::ₘ s)
theorem multiset.count_cons {α : Type u_1} [decidable_eq α] (a b : α) (s : multiset α) :
(b