Sum and difference of multisets

This file defines the following operations on multisets:

• Add (Multiset α) instance: s + t adds the multiplicities of the elements of s and t
• Sub (Multiset α) instance: s - t subtracts the multiplicities of the elements of s and t
• Multiset.erase: s.erase x reduces the multiplicity of x in s by one.

Notation (defined later)

• s + t: The multiset for which the number of occurrences of each a is the sum of the occurrences of a in s and t.
• s - t: The multiset for which the number of occurrences of each a is the difference of the occurrences of a in s and t.

Additive monoid

def Multiset.add {α : Type u_1} (s₁ s₂ : 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

• s₁.add s₂ = Quotient.liftOn₂ s₁ s₂ (fun (l₁ l₂ : List α) => ↑(l₁ ++ l₂)) ⋯

instance Multiset.instAdd {α : Type u_1} : Add (Multiset α)

Equations

• Multiset.instAdd = { add := Multiset.add }

@[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

theorem Multiset.add_le_add_iff_left {α : Type u_1} {s t u : Multiset α} : s + t ≤ s + u ↔ t ≤ u

theorem Multiset.add_le_add_iff_right {α : Type u_1} {s t u : Multiset α} : s + u ≤ t + u ↔ s ≤ t

theorem Multiset.le_of_add_le_add_left {α : Type u_1} {s t u : Multiset α} : s + t ≤ s + u → t ≤ u

Alias of the forward direction of Multiset.add_le_add_iff_left.

theorem Multiset.add_le_add_left {α : Type u_1} {s t u : Multiset α} : t ≤ u → s + t ≤ s + u

Alias of the reverse direction of Multiset.add_le_add_iff_left.

theorem Multiset.add_le_add_right {α : Type u_1} {s t u : Multiset α} : s ≤ t → s + u ≤ t + u

Alias of the reverse direction of Multiset.add_le_add_iff_right.

theorem Multiset.le_of_add_le_add_right {α : Type u_1} {s t u : Multiset α} : s + u ≤ t + u → s ≤ t

Alias of the forward direction of Multiset.add_le_add_iff_right.

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

theorem Multiset.add_assoc {α : Type u_1} (s t u : Multiset α) : s + t + u = s + (t + u)

@[simp]

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

@[simp]

theorem Multiset.add_zero {α : Type u_1} (s : Multiset α) : s + 0 = s

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.subset_add_left {α : Type u_1} {s t : Multiset α} : s ⊆ s + t

theorem Multiset.subset_add_right {α : 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

@[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

@[simp]

theorem Multiset.countP_add {α : Type u_1} (p : α → Prop) [DecidablePred p] (s t : Multiset α) : countP p (s + t) = countP p s + countP p t

@[simp]

theorem Multiset.count_add {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : count a (s + t) = count a s + count a t

theorem Multiset.add_left_inj {α : Type u_1} {s t u : Multiset α} : s + u = t + u ↔ s = t

theorem Multiset.add_right_inj {α : Type u_1} {s t u : Multiset α} : s + t = s + u ↔ t = u

@[simp]

theorem Multiset.card_add {α : Type u_1} (s t : Multiset α) : (s + t).card = s.card + t.card

Erasing one copy of an element

def Multiset.erase {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : Multiset α

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

Equations

• s.erase a = Quot.liftOn s (fun (l : List α) => ↑(l.erase a)) ⋯

@[simp]

theorem Multiset.coe_erase {α : Type u_1} [DecidableEq α] (l : List α) (a : α) : (↑l).erase a = ↑(l.erase a)

@[simp]

theorem Multiset.erase_zero {α : Type u_1} [DecidableEq α] (a : α) : erase 0 a = 0

@[simp]

theorem Multiset.erase_cons_head {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : (a ::ₘ s).erase a = s

@[simp]

theorem Multiset.erase_cons_tail {α : Type u_1} [DecidableEq α] {a b : α} (s : Multiset α) (h : b ≠ a) : (b ::ₘ s).erase a = b ::ₘ s.erase a

@[simp]

theorem Multiset.erase_singleton {α : Type u_1} [DecidableEq α] (a : α) : {a}.erase a = 0

@[simp]

theorem Multiset.erase_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : ¬a ∈ s → s.erase a = s

@[deprecated Multiset.erase_of_notMem (since := "2025-05-23")]

theorem Multiset.erase_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : ¬a ∈ s → s.erase a = s

Alias of Multiset.erase_of_notMem.

@[simp]

theorem Multiset.cons_erase {α : Type u_1} [DecidableEq α] {s : Multiset α} {a : α} : a ∈ s → a ::ₘ s.erase a = s

theorem Multiset.erase_cons_tail_of_mem {α : Type u_1} [DecidableEq α] {s : Multiset α} {a b : α} (h : a ∈ s) : (b ::ₘ s).erase a = b ::ₘ s.erase a

theorem Multiset.le_cons_erase {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : s ≤ a ::ₘ s.erase a

theorem Multiset.add_singleton_eq_iff {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} : s + {a} = t ↔ a ∈ t ∧ s = t.erase a

theorem Multiset.erase_add_left_pos {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (t : Multiset α) : a ∈ s → (s + t).erase a = s.erase a + t

theorem Multiset.erase_add_right_pos {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) (h : a ∈ t) : (s + t).erase a = s + t.erase a

theorem Multiset.erase_add_right_neg {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (t : Multiset α) : ¬a ∈ s → (s + t).erase a = s + t.erase a

theorem Multiset.erase_add_left_neg {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) (h : ¬a ∈ t) : (s + t).erase a = s.erase a + t

theorem Multiset.erase_le {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : s.erase a ≤ s

@[simp]

theorem Multiset.erase_lt {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : s.erase a < s ↔ a ∈ s

theorem Multiset.erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : s.erase a ⊆ s

theorem Multiset.mem_erase_of_ne {α : Type u_1} [DecidableEq α] {a b : α} {s : Multiset α} (ab : a ≠ b) : a ∈ s.erase b ↔ a ∈ s

theorem Multiset.mem_of_mem_erase {α : Type u_1} [DecidableEq α] {a b : α} {s : Multiset α} : a ∈ s.erase b → a ∈ s

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

instance Multiset.instRightCommutativeErase {α : Type u_1} [DecidableEq α] : RightCommutative erase

theorem Multiset.erase_le_erase {α : Type u_1} [DecidableEq α] {s t : Multiset α} (a : α) (h : s ≤ t) : s.erase a ≤ t.erase a

theorem Multiset.erase_le_iff_le_cons {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} : s.erase a ≤ t ↔ s ≤ a ::ₘ t

@[simp]

theorem Multiset.card_erase_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∈ s → (s.erase a).card = s.card.pred

theorem Multiset.card_erase_add_one {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∈ s → (s.erase a).card + 1 = s.card

theorem Multiset.card_erase_lt_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∈ s → (s.erase a).card < s.card

theorem Multiset.card_erase_le {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : (s.erase a).card ≤ s.card

theorem Multiset.card_erase_eq_ite {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : (s.erase a).card = if a ∈ s then s.card.pred else s.card

@[simp]

theorem Multiset.count_erase_self {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : count a (s.erase a) = count a s - 1

@[simp]

theorem Multiset.count_erase_of_ne {α : Type u_1} [DecidableEq α] {a b : α} (ab : a ≠ b) (s : Multiset α) : count a (s.erase b) = count a s

Subtraction

def Multiset.sub {α : Type u_1} [DecidableEq α] (s t : Multiset α) : 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 count a (s - t) = 0 if count a s ≤ count a t).

Equations

• s.sub t = Quotient.liftOn₂ s t (fun (l₁ l₂ : List α) => ↑(l₁.diff l₂)) ⋯

instance Multiset.instSub {α : Type u_1} [DecidableEq α] : Sub (Multiset α)

Equations

• Multiset.instSub = { sub := Multiset.sub }

@[simp]

theorem Multiset.coe_sub {α : Type u_1} [DecidableEq α] (s t : List α) : ↑s - ↑t = ↑(s.diff t)

@[simp]

theorem Multiset.sub_zero {α : Type u_1} [DecidableEq α] (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 OrderedSub (Multiset α).

@[simp]

theorem Multiset.sub_cons {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : s - a ::ₘ t = s.erase a - t

theorem Multiset.zero_sub {α : Type u_1} [DecidableEq α] (t : Multiset α) : 0 - t = 0

@[simp]

theorem Multiset.countP_sub {α : Type u_1} [DecidableEq α] {s t : Multiset α} : t ≤ s → ∀ (p : α → Prop) [inst : DecidablePred p], countP p (s - t) = countP p s - countP p t

@[simp]

theorem Multiset.count_sub {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : count a (s - t) = count a s - count a t

theorem Multiset.sub_le_iff_le_add {α : Type u_1} [DecidableEq α] {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 OrderedSub (Multiset α).

theorem Multiset.sub_le_iff_le_add' {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : s - t ≤ u ↔ s ≤ t + u

This is a special case of tsub_le_iff_left, which should be used instead of this.

theorem Multiset.sub_le_self {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s - t ≤ s

theorem Multiset.add_sub_assoc {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (hut : u ≤ t) : s + t - u = s + (t - u)

theorem Multiset.add_sub_cancel {α : Type u_1} [DecidableEq α] {s t : Multiset α} (hts : t ≤ s) : s - t + t = s

theorem Multiset.sub_add_cancel {α : Type u_1} [DecidableEq α] {s t : Multiset α} (hts : t ≤ s) : s - t + t = s

theorem Multiset.sub_add_eq_sub_sub {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : s - (t + u) = s - t - u

theorem Multiset.le_sub_add {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ≤ s - t + t

theorem Multiset.le_add_sub {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ≤ t + (s - t)

theorem Multiset.sub_le_sub_right {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (hst : s ≤ t) : s - u ≤ t - u

theorem Multiset.add_sub_cancel_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s + t - t = s

theorem Multiset.eq_sub_of_add_eq {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (hstu : s + t = u) : s = u - t

theorem Multiset.cons_sub_of_le {α : Type u_1} [DecidableEq α] (a : α) {s t : Multiset α} (h : t ≤ s) : a ::ₘ s - t = a ::ₘ (s - t)

@[simp]

theorem Multiset.card_sub {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : t ≤ s) : (s - t).card = s.card - t.card

@[simp]

theorem Multiset.sub_singleton {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : s - {a} = s.erase a

theorem Multiset.mem_sub {α : Type u_1} [DecidableEq α] {a : α} {s t : Multiset α} : a ∈ s - t ↔ count a t < count a s

Lift a relation to Multisets

theorem Multiset.Rel.add {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β} {u : Multiset α} {v : Multiset β} (hst : Rel r s t) (huv : Rel r u v) : Rel r (s + u) (t + v)

theorem Multiset.rel_add_left {α : Type u_1} {β : Type v} {r : α → β → Prop} {as₀ as₁ : Multiset α} {bs : Multiset β} : Rel r (as₀ + as₁) bs ↔ ∃ (bs₀ : Multiset β), ∃ (bs₁ : Multiset β), Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

theorem Multiset.rel_add_right {α : Type u_1} {β : Type v} {r : α → β → Prop} {as : Multiset α} {bs₀ bs₁ : Multiset β} : Rel r as (bs₀ + bs₁) ↔ ∃ (as₀ : Multiset α), ∃ (as₁ : Multiset α), Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

@[simp]

theorem Multiset.nodup_singleton {α : Type u_1} (a : α) : {a}.Nodup

theorem Multiset.not_nodup_pair {α : Type u_1} (a : α) : ¬(a ::ₘ a ::ₘ 0).Nodup

theorem Multiset.Nodup.erase {α : Type u_1} [DecidableEq α] (a : α) {l : Multiset α} : l.Nodup → (l.erase a).Nodup

theorem Multiset.mem_sub_of_nodup {α : Type u_1} [DecidableEq α] {a : α} {s t : Multiset α} (d : s.Nodup) : a ∈ s - t ↔ a ∈ s ∧ ¬a ∈ t