Mathlib.Data.Multiset.AddSub

Multiset.add definition

(s₁ s₂ : Multiset α) : Multiset α

Full source

/-- 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`. -/
protected def add (s₁ s₂ : Multiset α) : Multiset α :=
  (Quotient.liftOn₂ s₁ s₂ fun l₁ l₂ => ((l₁ ++ l₂ : List α) : Multiset α)) fun _ _ _ _ p₁ p₂ =>
    Quot.sound <| p₁.append p₂

Sum of multisets

Informal description

The sum of two multisets $ s $ and $ t $ is the multiset where the count of each element $ a $ is the sum of the counts of $ a $ in $ s $ and $ t $. Formally, for any element $ a $, we have $ \text{count}_a (s + t) = \text{count}_a s + \text{count}_a t $.

Multiset.instAdd instance

: Add (Multiset α)

Full source

instance : Add (Multiset α) :=
  ⟨Multiset.add⟩

Additive Structure on Multisets

Informal description

For any type $\alpha$, the collection of multisets over $\alpha$ forms an additive structure where the sum of two multisets $s$ and $t$ is defined by pointwise addition of their element counts. That is, for any element $a \in \alpha$, the count of $a$ in $s + t$ is the sum of the counts of $a$ in $s$ and $t$.

Multiset.coe_add theorem

(s t : List α) : (s + t : Multiset α) = (s ++ t : List α)

Full source

@[simp]
theorem coe_add (s t : List α) : (s + t : Multiset α) = (s ++ t : List α) :=
  rfl

Multiset Addition of Lists Equals List Concatenation

Informal description

For any two lists $s$ and $t$ of elements of type $\alpha$, the multiset obtained by adding their corresponding multisets is equal to the multiset obtained from the concatenation of the two lists. That is, $(s + t : \text{Multiset } \alpha) = (s \mathbin{+\kern-1.5ex+} t : \text{List } \alpha)$.

Multiset.singleton_add theorem

(a : α) (s : Multiset α) : { a } + s = a ::ₘ s

Full source

@[simp]
theorem singleton_add (a : α) (s : Multiset α) : {a} + s = a ::ₘ s :=
  rfl

Sum of Singleton Multiset Equals Insertion: $\{a\} + s = a \mathbin{::} s$

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the sum of the singleton multiset $\{a\}$ and $s$ is equal to the multiset obtained by inserting $a$ into $s$ (i.e., $\{a\} + s = a \mathbin{::} s$).

Multiset.add_le_add_iff_left theorem

: s + t ≤ s + u ↔ t ≤ u

Full source

protected lemma add_le_add_iff_left : s + t ≤ s + u ↔ t ≤ u :=
  Quotient.inductionOn₃ s t u fun _ _ _ => subperm_append_left _

Left Cancellation Property of Multiset Addition: $s + t \leq s + u \leftrightarrow t \leq u$

Informal description

For any multisets $s$, $t$, and $u$ over a type $\alpha$, the inequality $s + t \leq s + u$ holds if and only if $t \leq u$.

Multiset.add_le_add_iff_right theorem

: s + u ≤ t + u ↔ s ≤ t

Full source

protected lemma add_le_add_iff_right : s + u ≤ t + u ↔ s ≤ t :=
  Quotient.inductionOn₃ s t u fun _ _ _ => subperm_append_right _

Right Cancellation Property of Multiset Addition: $s + u \leq t + u \leftrightarrow s \leq t$

Informal description

For any multisets $s$, $t$, and $u$ over a type $\alpha$, the inequality $s + u \leq t + u$ holds if and only if $s \leq t$.

Multiset.add_comm theorem

(s t : Multiset α) : s + t = t + s

Full source

protected lemma add_comm (s t : Multiset α) : s + t = t + s :=
  Quotient.inductionOn₂ s t fun _ _ ↦ Quot.sound perm_append_comm

Commutativity of Multiset Addition: $s + t = t + s$

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the sum of $s$ and $t$ is equal to the sum of $t$ and $s$, i.e., $s + t = t + s$.

Multiset.add_assoc theorem

(s t u : Multiset α) : s + t + u = s + (t + u)

Full source

protected lemma add_assoc (s t u : Multiset α) : s + t + u = s + (t + u) :=
  Quotient.inductionOn₃ s t u fun _ _ _ ↦ congr_arg _ <| append_assoc ..

Associativity of Multiset Addition: $(s + t) + u = s + (t + u)$

Informal description

For any multisets $s$, $t$, and $u$ over a type $\alpha$, the sum operation is associative, i.e., $(s + t) + u = s + (t + u)$.

Multiset.zero_add theorem

(s : Multiset α) : 0 + s = s

Full source

@[simp high]
protected lemma zero_add (s : Multiset α) : 0 + s = s := Quotient.inductionOn s fun _ ↦ rfl

Left Additive Identity for Multisets: $0 + s = s$

Informal description

For any multiset $s$ over a type $\alpha$, the sum of the empty multiset $0$ and $s$ is equal to $s$, i.e., $0 + s = s$.

Multiset.add_zero theorem

(s : Multiset α) : s + 0 = s

Full source

@[simp high]
protected lemma add_zero (s : Multiset α) : s + 0 = s :=
  Quotient.inductionOn s fun l ↦ congr_arg _ <| append_nil l

Right Additive Identity for Multisets

Informal description

For any multiset $s$ over a type $\alpha$, the sum of $s$ and the empty multiset $0$ is equal to $s$, i.e., $s + 0 = s$.

Multiset.le_add_right theorem

(s t : Multiset α) : s ≤ s + t

Full source

lemma le_add_right (s t : Multiset α) : s ≤ s + t := by
  simpa using Multiset.add_le_add_left (zero_le t)

Right Addition Preserves Multiset Order: $s \leq s + t$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the multiset $s$ is less than or equal to the sum $s + t$ in the partial order of multisets.

Multiset.le_add_left theorem

(s t : Multiset α) : s ≤ t + s

Full source

lemma le_add_left (s t : Multiset α) : s ≤ t + s := by
  simpa using Multiset.add_le_add_right (zero_le t)

Left Addition Preserves Multiset Order: $s \leq t + s$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the multiset $s$ is less than or equal to the sum $t + s$ in the partial order of multisets.

Multiset.subset_add_left theorem

{s t : Multiset α} : s ⊆ s + t

Full source

lemma subset_add_left {s t : Multiset α} : s ⊆ s + t := subset_of_le <| le_add_right s t

Left Addition Preserves Multiset Inclusion: $s \subseteq s + t$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the multiset $s$ is a subset of the sum $s + t$ in the multiset inclusion order.

Multiset.subset_add_right theorem

{s t : Multiset α} : s ⊆ t + s

Full source

lemma subset_add_right {s t : Multiset α} : s ⊆ t + s := subset_of_le <| le_add_left s t

Right Addition Preserves Multiset Inclusion: $s \subseteq t + s$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the multiset $s$ is a subset of the sum $t + s$ in the multiset inclusion order.

Multiset.le_iff_exists_add theorem

{s t : Multiset α} : s ≤ t ↔ ∃ u, t = s + u

Full source

theorem le_iff_exists_add {s t : Multiset α} : s ≤ t ↔ ∃ u, t = s + u :=
  ⟨fun h =>
    leInductionOn h fun s =>
      let ⟨l, p⟩ := s.exists_perm_append
      ⟨l, Quot.sound p⟩,
    fun ⟨_u, e⟩ => e.symm ▸ le_add_right _ _⟩

Characterization of Multiset Order via Addition: $s \leq t \leftrightarrow \exists u, t = s + u$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the relation $s \leq t$ holds if and only if there exists a multiset $u$ such that $t = s + u$.

Multiset.cons_add theorem

(a : α) (s t : Multiset α) : a ::ₘ s + t = a ::ₘ (s + t)

Full source

@[simp]
theorem cons_add (a : α) (s t : Multiset α) : a ::ₘ s + t = a ::ₘ (s + t) := by
  rw [← singleton_add, ← singleton_add, Multiset.add_assoc]

Insertion Distributes Over Multiset Addition: $a \mathbin{::} s + t = a \mathbin{::} (s + t)$

Informal description

For any element $a$ of type $\alpha$ and any multisets $s$ and $t$ over $\alpha$, the sum of the multiset obtained by inserting $a$ into $s$ (denoted $a \mathbin{::} s$) with $t$ is equal to the multiset obtained by inserting $a$ into the sum of $s$ and $t$ (i.e., $a \mathbin{::} (s + t)$).

Multiset.add_cons theorem

(a : α) (s t : Multiset α) : s + a ::ₘ t = a ::ₘ (s + t)

Full source

@[simp]
theorem add_cons (a : α) (s t : Multiset α) : s + a ::ₘ t = a ::ₘ (s + t) := by
  rw [Multiset.add_comm, cons_add, Multiset.add_comm]

Insertion Distributes Over Multiset Addition (Right Variant): $s + (a \mathbin{::} t) = a \mathbin{::} (s + t)$

Informal description

For any element $a$ of type $\alpha$ and any multisets $s$ and $t$ over $\alpha$, the sum of $s$ and the multiset obtained by inserting $a$ into $t$ (denoted $a \mathbin{::} t$) is equal to the multiset obtained by inserting $a$ into the sum of $s$ and $t$ (i.e., $s + (a \mathbin{::} t) = a \mathbin{::} (s + t)$).

Multiset.mem_add theorem

{a : α} {s t : Multiset α} : a ∈ s + t ↔ a ∈ s ∨ a ∈ t

Full source

@[simp]
theorem mem_add {a : α} {s t : Multiset α} : a ∈ s + ta ∈ s + t ↔ a ∈ s ∨ a ∈ t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ => mem_append

Membership in Sum of Multisets is Union of Memberships

Informal description

For any element $a$ of type $\alpha$ and multisets $s$ and $t$ over $\alpha$, the element $a$ belongs to the sum $s + t$ if and only if $a$ belongs to $s$ or $a$ belongs to $t$.

Multiset.countP_add theorem

(s t) : countP p (s + t) = countP p s + countP p t

Full source

@[simp]
theorem countP_add (s t) : countP p (s + t) = countP p s + countP p t :=
  Quotient.inductionOn₂ s t fun _ _ => countP_append

Additivity of Count with Respect to Multiset Addition

Informal description

For any predicate $p$ and multisets $s$ and $t$ over a type $\alpha$, the count of elements in $s + t$ satisfying $p$ is equal to the sum of the counts of elements satisfying $p$ in $s$ and $t$, i.e., \[ \text{countP}_p(s + t) = \text{countP}_p(s) + \text{countP}_p(t). \]

Multiset.count_add theorem

(a : α) : ∀ s t, count a (s + t) = count a s + count a t

Full source

@[simp]
theorem count_add (a : α) : ∀ s t, count a (s + t) = count a s + count a t :=
  countP_add _

Additivity of Element Count in Multiset Sum

Informal description

For any element $a$ of type $\alpha$ and multisets $s$ and $t$ over $\alpha$, the multiplicity of $a$ in the sum $s + t$ is equal to the sum of the multiplicities of $a$ in $s$ and $t$, i.e., \[ \text{count}(a, s + t) = \text{count}(a, s) + \text{count}(a, t). \]

Multiset.add_left_inj theorem

: s + u = t + u ↔ s = t

Full source

protected lemma add_left_inj : s + u = t + u ↔ s = t := by classical simp [Multiset.ext]

Left Cancellation Law for Multiset Addition: $s + u = t + u \leftrightarrow s = t$

Informal description

For any multisets $s$, $t$, and $u$ over a type $\alpha$, the equality $s + u = t + u$ holds if and only if $s = t$.

Multiset.add_right_inj theorem

: s + t = s + u ↔ t = u

Full source

protected lemma add_right_inj : s + t = s + u ↔ t = u := by classical simp [Multiset.ext]

Right Cancellation Law for Multiset Addition: $s + t = s + u \leftrightarrow t = u$

Informal description

For any multisets $s$, $t$, and $u$ over a type $\alpha$, the equality $s + t = s + u$ holds if and only if $t = u$.

Multiset.card_add theorem

(s t : Multiset α) : card (s + t) = card s + card t

Full source

@[simp]
theorem card_add (s t : Multiset α) : card (s + t) = card s + card t :=
  Quotient.inductionOn₂ s t fun _ _ => length_append

Cardinality of Multiset Sum: $|s + t| = |s| + |t|$

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the cardinality of their sum $s + t$ is equal to the sum of their individual cardinalities, i.e., $|s + t| = |s| + |t|$.

Multiset.erase definition

(s : Multiset α) (a : α) : Multiset α

Full source

/-- `erase s a` is the multiset that subtracts 1 from the multiplicity of `a`. -/
def erase (s : Multiset α) (a : α) : Multiset α :=
  Quot.liftOn s (fun l => (l.erase a : Multiset α)) fun _l₁ _l₂ p => Quot.sound (p.erase a)

Multiset element erasure

Informal description

For a multiset $ s $ over a type $ \alpha $ and an element $ a \in \alpha $, the operation $ \text{erase}(s, a) $ returns a new multiset where the multiplicity of $ a $ is decreased by one (if $ a $ was present in $ s $).

Multiset.coe_erase theorem

(l : List α) (a : α) : erase (l : Multiset α) a = l.erase a

Full source

@[simp]
theorem coe_erase (l : List α) (a : α) : erase (l : Multiset α) a = l.erase a :=
  rfl

Coercion and Erasure Commute for Multisets and Lists

Informal description

For any list $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the multiset obtained by coercing $l$ to a multiset and then erasing one occurrence of $a$ is equal to the multiset obtained by coercing the list $l.erase a$ (where $l.erase a$ removes one occurrence of $a$ from $l$).

Multiset.erase_zero theorem

(a : α) : (0 : Multiset α).erase a = 0

Full source

@[simp]
theorem erase_zero (a : α) : (0 : Multiset α).erase a = 0 :=
  rfl

Erasure from Empty Multiset Yields Empty Multiset

Informal description

For any element $a$ of type $\alpha$, erasing one occurrence of $a$ from the empty multiset $0$ yields the empty multiset $0$ again. That is, $\text{erase}(0, a) = 0$.

Multiset.erase_cons_head theorem

(a : α) (s : Multiset α) : (a ::ₘ s).erase a = s

Full source

@[simp]
theorem erase_cons_head (a : α) (s : Multiset α) : (a ::ₘ s).erase a = s :=
  Quot.inductionOn s fun l => congr_arg _ <| List.erase_cons_head a l

Erasure of Head Element in Multiset Insertion

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, erasing one occurrence of $a$ from the multiset obtained by inserting $a$ into $s$ yields the original multiset $s$. That is, $\text{erase}(a \text{ ::ₘ } s, a) = s$.

Multiset.erase_cons_tail theorem

{a b : α} (s : Multiset α) (h : b ≠ a) : (b ::ₘ s).erase a = b ::ₘ s.erase a

Full source

@[simp]
theorem erase_cons_tail {a b : α} (s : Multiset α) (h : b ≠ a) :
    (b ::ₘ s).erase a = b ::ₘ s.erase a :=
  Quot.inductionOn s fun _ => congr_arg _ <| List.erase_cons_tail (not_beq_of_ne h)

Erasing a distinct element from a multiset insertion

Informal description

For any distinct elements $a$ and $b$ of type $\alpha$ and any multiset $s$ over $\alpha$, the operation of erasing $a$ from the multiset obtained by inserting $b$ into $s$ is equal to inserting $b$ into the multiset obtained by erasing $a$ from $s$. In symbols, if $b \neq a$, then $(b \cup s) \setminus a = b \cup (s \setminus a)$.

Multiset.erase_singleton theorem

(a : α) : ({ a } : Multiset α).erase a = 0

Full source

@[simp]
theorem erase_singleton (a : α) : ({a} : Multiset α).erase a = 0 :=
  erase_cons_head a 0

Erasure from Singleton Multiset Yields Empty Multiset

Informal description

For any element $a$ of type $\alpha$, erasing one occurrence of $a$ from the singleton multiset $\{a\}$ results in the empty multiset $0$. That is, $\text{erase}(\{a\}, a) = 0$.

Multiset.erase_of_not_mem theorem

{a : α} {s : Multiset α} : a ∉ s → s.erase a = s

Full source

@[simp]
theorem erase_of_not_mem {a : α} {s : Multiset α} : a ∉ s → s.erase a = s :=
  Quot.inductionOn s fun _l h => congr_arg _ <| List.erase_of_not_mem h

Erasure of Non-member Element Leaves Multiset Unchanged

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ is not a member of $s$, then erasing one occurrence of $a$ from $s$ leaves $s$ unchanged, i.e., $\text{erase}(s, a) = s$.

Multiset.cons_erase theorem

{s : Multiset α} {a : α} : a ∈ s → a ::ₘ s.erase a = s

Full source

@[simp]
theorem cons_erase {s : Multiset α} {a : α} : a ∈ s → a ::ₘ s.erase a = s :=
  Quot.inductionOn s fun _l h => Quot.sound (perm_cons_erase h).symm

Reconstruction of Multiset via Insertion and Erasure

Informal description

For any multiset $s$ over a type $\alpha$ and any element $a \in \alpha$ that is present in $s$, the operation of inserting $a$ into the multiset obtained by erasing one occurrence of $a$ from $s$ yields the original multiset $s$. In other words, $a \text{ ::ₘ } \text{erase}(s, a) = s$ when $a \in s$.

Multiset.erase_cons_tail_of_mem theorem

(h : a ∈ s) : (b ::ₘ s).erase a = b ::ₘ s.erase a

Full source

theorem erase_cons_tail_of_mem (h : a ∈ s) :
    (b ::ₘ s).erase a = b ::ₘ s.erase a := by
  rcases eq_or_ne a b with rfl | hab
  · simp [cons_erase h]
  · exact s.erase_cons_tail hab.symm

Erasure commutes with insertion for elements in a multiset

Informal description

For any element $a$ in a multiset $s$ over a type $\alpha$, and for any element $b$ of $\alpha$, erasing one occurrence of $a$ from the multiset obtained by inserting $b$ into $s$ is equal to inserting $b$ into the multiset obtained by erasing one occurrence of $a$ from $s$. In symbols, if $a \in s$, then $(b \cup s) \setminus a = b \cup (s \setminus a)$.

Multiset.le_cons_erase theorem

(s : Multiset α) (a : α) : s ≤ a ::ₘ s.erase a

Full source

theorem le_cons_erase (s : Multiset α) (a : α) : s ≤ a ::ₘ s.erase a :=
  if h : a ∈ s then le_of_eq (cons_erase h).symm
  else by rw [erase_of_not_mem h]; apply le_cons_self

Submultiset Property: $s \leq a \text{ ::ₘ } s.\text{erase}(a)$

Informal description

For any multiset $s$ over a type $\alpha$ and any element $a \in \alpha$, the multiset $s$ is contained in the multiset obtained by inserting $a$ into the multiset resulting from erasing one occurrence of $a$ from $s$, i.e., $s \leq a \text{ ::ₘ } s.\text{erase}(a)$.

Multiset.add_singleton_eq_iff theorem

{s t : Multiset α} {a : α} : s + { a } = t ↔ a ∈ t ∧ s = t.erase a

Full source

theorem add_singleton_eq_iff {s t : Multiset α} {a : α} : s + {a} = t ↔ a ∈ t ∧ s = t.erase a := by
  rw [Multiset.add_comm, singleton_add]
  constructor
  · rintro rfl
    exact ⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩
  · rintro ⟨h, rfl⟩
    exact cons_erase h

Characterization of Multiset Sum with Singleton: $s + \{a\} = t \leftrightarrow (a \in t \land s = t \setminus a)$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$ and any element $a \in \alpha$, the sum $s + \{a\}$ equals $t$ if and only if $a$ is an element of $t$ and $s$ equals $t$ with one occurrence of $a$ removed, i.e., $s + \{a\} = t \leftrightarrow (a \in t \land s = t.\text{erase}(a))$.

Multiset.erase_add_left_pos theorem

{a : α} {s : Multiset α} (t) : a ∈ s → (s + t).erase a = s.erase a + t

Full source

theorem erase_add_left_pos {a : α} {s : Multiset α} (t) : a ∈ s → (s + t).erase a = s.erase a + t :=
  Quotient.inductionOn₂ s t fun _l₁ l₂ h => congr_arg _ <| erase_append_left l₂ h

Erasing from Sum of Multisets When Element in First Operand

Informal description

For any element $a$ in a type $\alpha$, any multiset $s$ over $\alpha$ containing $a$, and any multiset $t$ over $\alpha$, the operation of erasing one occurrence of $a$ from the sum $s + t$ is equal to the sum of the result of erasing one occurrence of $a$ from $s$ and $t$, i.e., $(s + t).\text{erase}(a) = s.\text{erase}(a) + t$.

Multiset.erase_add_right_pos theorem

{a : α} (s) (h : a ∈ t) : (s + t).erase a = s + t.erase a

Full source

theorem erase_add_right_pos {a : α} (s) (h : a ∈ t) : (s + t).erase a = s + t.erase a := by
  rw [Multiset.add_comm, erase_add_left_pos s h, Multiset.add_comm]

Erasing from Sum of Multisets When Element in Second Operand

Informal description

For any element $a$ in a type $\alpha$, any multiset $s$ over $\alpha$, and any multiset $t$ over $\alpha$ containing $a$, the operation of erasing one occurrence of $a$ from the sum $s + t$ is equal to the sum of $s$ and the result of erasing one occurrence of $a$ from $t$, i.e., $(s + t).\text{erase}(a) = s + t.\text{erase}(a)$.

Multiset.erase_add_right_neg theorem

{a : α} {s : Multiset α} (t) : a ∉ s → (s + t).erase a = s + t.erase a

Full source

theorem erase_add_right_neg {a : α} {s : Multiset α} (t) :
    a ∉ s → (s + t).erase a = s + t.erase a :=
  Quotient.inductionOn₂ s t fun _l₁ l₂ h => congr_arg _ <| erase_append_right l₂ h

Erasing from Sum of Multisets When Element Not in First Operand

Informal description

For any element $a$ in a type $\alpha$, any multiset $s$ over $\alpha$ not containing $a$, and any multiset $t$ over $\alpha$, the operation of erasing one occurrence of $a$ from the sum $s + t$ is equal to the sum of $s$ and the result of erasing one occurrence of $a$ from $t$, i.e., $(s + t).\text{erase}(a) = s + t.\text{erase}(a)$.

Multiset.erase_add_left_neg theorem

{a : α} (s) (h : a ∉ t) : (s + t).erase a = s.erase a + t

Full source

theorem erase_add_left_neg {a : α} (s) (h : a ∉ t) : (s + t).erase a = s.erase a + t := by
  rw [Multiset.add_comm, erase_add_right_neg s h, Multiset.add_comm]

Erasing from Sum of Multisets When Element Not in Second Operand: $(s + t).\text{erase}(a) = s.\text{erase}(a) + t$

Informal description

For any element $a$ in a type $\alpha$, any multiset $s$ over $\alpha$, and any multiset $t$ over $\alpha$ not containing $a$, the operation of erasing one occurrence of $a$ from the sum $s + t$ is equal to the sum of the result of erasing one occurrence of $a$ from $s$ and $t$, i.e., $(s + t).\text{erase}(a) = s.\text{erase}(a) + t$.

Multiset.erase_le theorem

(a : α) (s : Multiset α) : s.erase a ≤ s

Full source

theorem erase_le (a : α) (s : Multiset α) : s.erase a ≤ s :=
  Quot.inductionOn s fun _ => erase_sublist.subperm

Submultiset Property of Multiset Erasure

Informal description

For any element $a$ in a type $\alpha$ and any multiset $s$ over $\alpha$, the multiset obtained by erasing one occurrence of $a$ from $s$ is a submultiset of $s$, i.e., $s.\text{erase}(a) \leq s$.

Multiset.erase_lt theorem

{a : α} {s : Multiset α} : s.erase a < s ↔ a ∈ s

Full source

@[simp]
theorem erase_lt {a : α} {s : Multiset α} : s.erase a < s ↔ a ∈ s :=
  ⟨fun h => not_imp_comm.1 erase_of_not_mem (ne_of_lt h), fun h => by
    simpa [h] using lt_cons_self (s.erase a) a⟩

Strict Submultiset Condition for Erasure: $s \setminus \{a\} < s \leftrightarrow a \in s$

Informal description

For any element $a$ in a type $\alpha$ and any multiset $s$ over $\alpha$, the multiset obtained by erasing one occurrence of $a$ from $s$ is strictly smaller than $s$ if and only if $a$ is an element of $s$. In other words, $s \setminus \{a\} < s \leftrightarrow a \in s$.

Multiset.erase_subset theorem

(a : α) (s : Multiset α) : s.erase a ⊆ s

Full source

theorem erase_subset (a : α) (s : Multiset α) : s.erase a ⊆ s :=
  subset_of_le (erase_le a s)

Subset Property of Multiset Erasure

Informal description

For any element $a$ in a type $\alpha$ and any multiset $s$ over $\alpha$, the multiset obtained by erasing one occurrence of $a$ from $s$ is a subset of $s$, i.e., $\text{erase}(s, a) \subseteq s$.

Multiset.mem_erase_of_ne theorem

{a b : α} {s : Multiset α} (ab : a ≠ b) : a ∈ s.erase b ↔ a ∈ s

Full source

theorem mem_erase_of_ne {a b : α} {s : Multiset α} (ab : a ≠ b) : a ∈ s.erase ba ∈ s.erase b ↔ a ∈ s :=
  Quot.inductionOn s fun _l => List.mem_erase_of_ne ab

Membership Preservation in Multiset Erasure for Distinct Elements

Informal description

For any distinct elements $a$ and $b$ in a type $\alpha$, and for any multiset $s$ over $\alpha$, the element $a$ belongs to the multiset obtained by erasing one occurrence of $b$ from $s$ if and only if $a$ belongs to $s$. In other words, $a \in s \setminus \{b\} \leftrightarrow a \in s$ when $a \neq b$.

Multiset.mem_of_mem_erase theorem

{a b : α} {s : Multiset α} : a ∈ s.erase b → a ∈ s

Full source

theorem mem_of_mem_erase {a b : α} {s : Multiset α} : a ∈ s.erase b → a ∈ s :=
  mem_of_subset (erase_subset _ _)

Membership Preservation under Multiset Erasure

Informal description

For any elements $a$ and $b$ in a type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ belongs to the multiset obtained by erasing one occurrence of $b$ from $s$, then $a$ belongs to $s$.

Multiset.erase_comm theorem

(s : Multiset α) (a b : α) : (s.erase a).erase b = (s.erase b).erase a

Full source

theorem erase_comm (s : Multiset α) (a b : α) : (s.erase a).erase b = (s.erase b).erase a :=
  Quot.inductionOn s fun l => congr_arg _ <| l.erase_comm a b

Commutativity of Multiset Erasure Operations

Informal description

For any multiset $s$ over a type $\alpha$ and any two distinct elements $a, b \in \alpha$, the operation of erasing $a$ followed by erasing $b$ from $s$ is equal to erasing $b$ followed by erasing $a$, i.e., $(s \setminus \{a\}) \setminus \{b\} = (s \setminus \{b\}) \setminus \{a\}$.

Multiset.instRightCommutativeErase instance

: RightCommutative erase (α := α)

Full source

instance : RightCommutative erase (α := α) := ⟨erase_comm⟩

Right Commutativity of Multiset Erasure

Informal description

For any type $\alpha$, the operation of erasing an element from a multiset is right-commutative. That is, for any multiset $s$ over $\alpha$ and any two elements $a, b \in \alpha$, we have $(s \setminus \{a\}) \setminus \{b\} = (s \setminus \{b\}) \setminus \{a\}$.

Multiset.erase_le_erase theorem

{s t : Multiset α} (a : α) (h : s ≤ t) : s.erase a ≤ t.erase a

Full source

@[gcongr]
theorem erase_le_erase {s t : Multiset α} (a : α) (h : s ≤ t) : s.erase a ≤ t.erase a :=
  leInductionOn h fun h => (h.erase _).subperm

Monotonicity of Multiset Erasure with Respect to Submultiset Ordering

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, if $s$ is a submultiset of $t$ (i.e., $s \leq t$), then for any element $a \in \alpha$, the erasure of $a$ from $s$ is a submultiset of the erasure of $a$ from $t$, i.e., $s.\text{erase}(a) \leq t.\text{erase}(a)$.

Multiset.erase_le_iff_le_cons theorem

{s t : Multiset α} {a : α} : s.erase a ≤ t ↔ s ≤ a ::ₘ t

Full source

theorem erase_le_iff_le_cons {s t : Multiset α} {a : α} : s.erase a ≤ t ↔ s ≤ a ::ₘ t :=
  ⟨fun h => le_trans (le_cons_erase _ _) (cons_le_cons _ h), fun h =>
    if m : a ∈ s then by rw [← cons_erase m] at h; exact (cons_le_cons_iff _).1 h
    else le_trans (erase_le _ _) ((le_cons_of_not_mem m).1 h)⟩

Submultiset Condition for Erasure and Insertion: $s \setminus \{a\} \leq t \leftrightarrow s \leq a \text{ ::ₘ } t$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$ and any element $a \in \alpha$, the multiset obtained by erasing one occurrence of $a$ from $s$ is a submultiset of $t$ if and only if $s$ is a submultiset of the multiset obtained by inserting $a$ into $t$. In other words, $s \setminus \{a\} \leq t \leftrightarrow s \leq a \text{ ::ₘ } t$.

Multiset.card_erase_of_mem theorem

{a : α} {s : Multiset α} : a ∈ s → card (s.erase a) = pred (card s)

Full source

@[simp]
theorem card_erase_of_mem {a : α} {s : Multiset α} : a ∈ s → card (s.erase a) = pred (card s) :=
  Quot.inductionOn s fun _l => length_erase_of_mem

Cardinality of Multiset After Erasure: $|s \setminus \{a\}| = |s| - 1$ when $a \in s$

Informal description

For any element $a$ in a multiset $s$ over a type $\alpha$, the cardinality of the multiset obtained by erasing one occurrence of $a$ from $s$ is equal to the predecessor of the cardinality of $s$, i.e., $|s \setminus \{a\}| = |s| - 1$.

Multiset.card_erase_add_one theorem

{a : α} {s : Multiset α} : a ∈ s → card (s.erase a) + 1 = card s

Full source

@[simp]
theorem card_erase_add_one {a : α} {s : Multiset α} : a ∈ s → card (s.erase a) + 1 = card s :=
  Quot.inductionOn s fun _l => length_erase_add_one

Cardinality of Multiset After Erasure Plus One Equals Original Cardinality

Informal description

For any element $a$ in a multiset $s$ over a type $\alpha$, the cardinality of the multiset obtained by erasing one occurrence of $a$ from $s$ plus one equals the cardinality of $s$, i.e., $|s \setminus \{a\}| + 1 = |s|$.

Multiset.card_erase_lt_of_mem theorem

{a : α} {s : Multiset α} : a ∈ s → card (s.erase a) < card s

Full source

theorem card_erase_lt_of_mem {a : α} {s : Multiset α} : a ∈ s → card (s.erase a) < card s :=
  fun h => card_lt_card (erase_lt.mpr h)

Strict Cardinality Decrease Under Multiset Erasure: $|s \setminus \{a\}| < |s|$ when $a \in s$

Informal description

For any element $a$ in a multiset $s$ over a type $\alpha$, if $a$ is an element of $s$, then the cardinality of the multiset obtained by erasing one occurrence of $a$ from $s$ is strictly less than the cardinality of $s$, i.e., $|s \setminus \{a\}| < |s|$.

Multiset.card_erase_le theorem

{a : α} {s : Multiset α} : card (s.erase a) ≤ card s

Full source

theorem card_erase_le {a : α} {s : Multiset α} : card (s.erase a) ≤ card s :=
  card_le_card (erase_le a s)

Cardinality Non-Increasing Under Multiset Erasure

Informal description

For any element $a$ in a type $\alpha$ and any multiset $s$ over $\alpha$, the cardinality of the multiset obtained by erasing one occurrence of $a$ from $s$ is less than or equal to the cardinality of $s$, i.e., $|s \setminus \{a\}| \leq |s|$.

Multiset.card_erase_eq_ite theorem

{a : α} {s : Multiset α} : card (s.erase a) = if a ∈ s then pred (card s) else card s

Full source

theorem card_erase_eq_ite {a : α} {s : Multiset α} :
    card (s.erase a) = if a ∈ s then pred (card s) else card s := by
  by_cases h : a ∈ s
  · rwa [card_erase_of_mem h, if_pos]
  · rwa [erase_of_not_mem h, if_neg]

Cardinality of Multiset After Conditional Erasure: $|s \setminus \{a\}| = |s| - 1$ if $a \in s$, else $|s|$

Informal description

For any element $a$ in a type $\alpha$ and any multiset $s$ over $\alpha$, the cardinality of the multiset obtained by erasing one occurrence of $a$ from $s$ is equal to $|s| - 1$ if $a \in s$, and remains $|s|$ otherwise. In other words: $$|s \setminus \{a\}| = \begin{cases} |s| - 1 & \text{if } a \in s \\ |s| & \text{otherwise} \end{cases}$$

Multiset.count_erase_self theorem

(a : α) (s : Multiset α) : count a (erase s a) = count a s - 1

Full source

@[simp]
theorem count_erase_self (a : α) (s : Multiset α) : count a (erase s a) = count a s - 1 :=
  Quotient.inductionOn s fun l => by
    convert List.count_erase_self (a := a) (l := l) <;> rw [← coe_count] <;> simp

Multiplicity Reduction Under Self-Erasure: $\text{count}_a (\text{erase } s a) = \text{count}_a s - 1$

Informal description

For any element $a$ in a type $\alpha$ and any multiset $s$ over $\alpha$, the multiplicity of $a$ in the multiset obtained by erasing one occurrence of $a$ from $s$ is equal to the multiplicity of $a$ in $s$ minus one, i.e., $\text{count}_a (\text{erase } s a) = \text{count}_a s - 1$.

Multiset.count_erase_of_ne theorem

{a b : α} (ab : a ≠ b) (s : Multiset α) : count a (erase s b) = count a s

Full source

@[simp]
theorem count_erase_of_ne {a b : α} (ab : a ≠ b) (s : Multiset α) :
    count a (erase s b) = count a s :=
  Quotient.inductionOn s fun l => by
    convert List.count_erase_of_ne ab (l := l) <;> rw [← coe_count] <;> simp

Multiplicity Preservation Under Non-Self Erasure: $\text{count}_a (\text{erase } s b) = \text{count}_a s$ for $a \neq b$

Informal description

For any distinct elements $a$ and $b$ in a type $\alpha$ and any multiset $s$ over $\alpha$, the multiplicity of $a$ in the multiset obtained by erasing one occurrence of $b$ from $s$ is equal to the multiplicity of $a$ in $s$, i.e., $\text{count}_a (\text{erase } s b) = \text{count}_a s$.

Multiset.sub definition

(s t : Multiset α) : Multiset α

Full source

/-- `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`). -/
protected def sub (s t : Multiset α) : Multiset α :=
  (Quotient.liftOn₂ s t fun l₁ l₂ => (l₁.diff l₂ : Multiset α)) fun _v₁ _v₂ _w₁ _w₂ p₁ p₂ =>
    Quot.sound <| p₁.diff p₂

Difference of multisets

Informal description

For two multisets $s$ and $t$ over a type $\alpha$, the difference $s - t$ is the multiset where the count of each element $a$ is given by the truncated subtraction of the counts in $t$ from the counts in $s$. Specifically, $\text{count}_a (s - t) = \max(0, \text{count}_a s - \text{count}_a t)$ for every $a \in \alpha$.

Multiset.instSub instance

: Sub (Multiset α)

Full source

instance : Sub (Multiset α) := ⟨.sub⟩

Subtraction Operation on Multisets

Informal description

For any type $\alpha$, the multiset over $\alpha$ has a subtraction operation where for two multisets $s$ and $t$, the count of each element $a$ in $s - t$ is given by the truncated subtraction of the counts in $t$ from the counts in $s$. Specifically, $\text{count}_a (s - t) = \max(0, \text{count}_a s - \text{count}_a t)$ for every $a \in \alpha$.

Multiset.coe_sub theorem

(s t : List α) : (s - t : Multiset α) = s.diff t

Full source

@[simp]
lemma coe_sub (s t : List α) : (s - t : Multiset α) = s.diff t :=
  rfl

Multiset Difference of Lists Equals List Difference as Multiset

Informal description

For any two lists $s$ and $t$ over a type $\alpha$, the multiset difference $s - t$ (where $s$ and $t$ are implicitly coerced to multisets) is equal to the multiset obtained from the list difference $s.diff t$.

Multiset.sub_zero theorem

(s : Multiset α) : s - 0 = s

Full source

/-- This is a special case of `tsub_zero`, which should be used instead of this.
This is needed to prove `OrderedSub (Multiset α)`. -/
@[simp high]
protected lemma sub_zero (s : Multiset α) : s - 0 = s :=
  Quot.inductionOn s fun _l => rfl

Subtracting Zero Multiset is Identity

Informal description

For any multiset $s$ over a type $\alpha$, subtracting the empty multiset $0$ from $s$ leaves $s$ unchanged, i.e., $s - 0 = s$.

Multiset.sub_cons theorem

(a : α) (s t : Multiset α) : s - a ::ₘ t = s.erase a - t

Full source

@[simp]
lemma sub_cons (a : α) (s t : Multiset α) : s - a ::ₘ t = s.erase a - t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ => congr_arg _ <| diff_cons _ _ _

Subtraction of Cons Multiset Equals Erase then Subtract

Informal description

For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$, the subtraction of the multiset $a$ cons $t$ from $s$ equals the subtraction of $t$ from the multiset obtained by erasing one occurrence of $a$ from $s$. In symbols: \[ s - (a \cup t) = (s \setminus \{a\}) - t \] where $\cup$ denotes multiset union (addition) and $\setminus$ denotes the erase operation.

Multiset.zero_sub theorem

(t : Multiset α) : 0 - t = 0

Full source

protected lemma zero_sub (t : Multiset α) : 0 - t = 0 :=
  Multiset.induction_on t rfl fun a s ih => by simp [ih]

Subtraction of Any Multiset from Zero Multiset Yields Zero

Informal description

For any multiset $t$ over a type $\alpha$, the difference between the empty multiset $0$ and $t$ is the empty multiset, i.e., $0 - t = 0$.

Multiset.countP_sub theorem

{s t : Multiset α} : t ≤ s → ∀ (p : α → Prop) [DecidablePred p], countP p (s - t) = countP p s - countP p t

Full source

@[simp]
lemma countP_sub {s t : Multiset α} :
    t ≤ s → ∀ (p : α → Prop) [DecidablePred p], countP p (s - t) = countP p s - countP p t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ hl _ _ ↦ List.countP_diff hl _

Count Preservation under Multiset Subtraction

Informal description

For any multisets $s$ and $t$ over a type $\alpha$ such that $t$ is a submultiset of $s$, and for any decidable predicate $p$ on $\alpha$, the count of elements satisfying $p$ in the difference multiset $s - t$ equals the difference between the counts in $s$ and $t$. That is, \[ \text{count}_p (s - t) = \text{count}_p s - \text{count}_p t. \]

Multiset.count_sub theorem

(a : α) (s t : Multiset α) : count a (s - t) = count a s - count a t

Full source

@[simp]
lemma count_sub (a : α) (s t : Multiset α) : count a (s - t) = count a s - count a t :=
  Quotient.inductionOn₂ s t <| by simp [List.count_diff]

Multiplicity Preservation under Multiset Subtraction: $\text{count}_a (s - t) = \text{count}_a s - \text{count}_a t$

Informal description

For any element $a$ of type $\alpha$ and any multisets $s$ and $t$ over $\alpha$, the multiplicity of $a$ in the difference multiset $s - t$ is equal to the difference of the multiplicities of $a$ in $s$ and $t$. That is, \[ \text{count}_a (s - t) = \text{count}_a s - \text{count}_a t. \]

Multiset.sub_le_iff_le_add theorem

: s - t ≤ u ↔ s ≤ u + t

Full source

/-- This is a special case of `tsub_le_iff_right`, which should be used instead of this.
This is needed to prove `OrderedSub (Multiset α)`. -/
protected lemma sub_le_iff_le_add : s - t ≤ u ↔ s ≤ u + t := by
  induction t using Multiset.induction_on generalizing s with
  | empty => simp [Multiset.sub_zero]
  | cons a s IH => simp [IH, erase_le_iff_le_cons]

Submultiset Condition for Multiset Subtraction: $s - t \leq u \leftrightarrow s \leq u + t$

Informal description

For any multisets $s$, $t$, and $u$ over a type $\alpha$, the difference $s - t$ is a submultiset of $u$ if and only if $s$ is a submultiset of the sum $u + t$.

Multiset.sub_le_iff_le_add' theorem

: s - t ≤ u ↔ s ≤ t + u

Full source

/-- This is a special case of `tsub_le_iff_left`, which should be used instead of this. -/
protected lemma sub_le_iff_le_add' : s - t ≤ u ↔ s ≤ t + u := by
  rw [Multiset.sub_le_iff_le_add, Multiset.add_comm]

Submultiset Condition for Multiset Subtraction (variant): $s - t \leq u \leftrightarrow s \leq t + u$

Informal description

For any multisets $s$, $t$, and $u$ over a type $\alpha$, the difference $s - t$ is a submultiset of $u$ if and only if $s$ is a submultiset of the sum $t + u$.

Multiset.sub_le_self theorem

(s t : Multiset α) : s - t ≤ s

Full source

protected theorem sub_le_self (s t : Multiset α) : s - t ≤ s := by
  rw [Multiset.sub_le_iff_le_add]
  exact le_add_right _ _

Submultiset Property of Multiset Subtraction: $s - t \leq s$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the difference $s - t$ is a submultiset of $s$, i.e., $s - t \leq s$.

Multiset.add_sub_assoc theorem

(hut : u ≤ t) : s + t - u = s + (t - u)

Full source

protected lemma add_sub_assoc (hut : u ≤ t) : s + t - u = s + (t - u) := by
  ext a; simp [Nat.add_sub_assoc <| count_le_of_le _ hut]

Associativity of Multiset Addition and Subtraction: $(s + t) - u = s + (t - u)$ when $u \leq t$

Informal description

For any multisets $s$, $t$, and $u$ over a type $\alpha$, if $u$ is a submultiset of $t$ (i.e., $u \leq t$), then the following equality holds: \[ (s + t) - u = s + (t - u). \]

Multiset.add_sub_cancel theorem

(hts : t ≤ s) : s - t + t = s

Full source

protected lemma add_sub_cancel (hts : t ≤ s) : s - t + t = s := by
  ext a; simp [Nat.sub_add_cancel <| count_le_of_le _ hts]

Cancellation Law for Multiset Subtraction and Addition: $(s - t) + t = s$ when $t \leq s$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, if $t$ is a submultiset of $s$ (i.e., $t \leq s$), then $(s - t) + t = s$.

Multiset.sub_add_cancel theorem

(hts : t ≤ s) : s - t + t = s

Full source

protected lemma sub_add_cancel (hts : t ≤ s) : s - t + t = s := by
  ext a; simp [Nat.sub_add_cancel <| count_le_of_le _ hts]

Submultiset Cancellation: $(s - t) + t = s$ when $t \leq s$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, if $t$ is a submultiset of $s$ (i.e., $t \leq s$), then the operation of subtracting $t$ from $s$ and then adding $t$ back recovers the original multiset $s$. In other words, $(s - t) + t = s$.

Multiset.sub_add_eq_sub_sub theorem

: s - (t + u) = s - t - u

Full source

protected lemma sub_add_eq_sub_sub : s - (t + u) = s - t - u := by ext; simp [Nat.sub_add_eq]

Subtraction of Multiset Sums: $s - (t + u) = s - t - u$

Informal description

For any multisets $s$, $t$, and $u$ over a type $\alpha$, the difference $s - (t + u)$ is equal to the iterated difference $(s - t) - u$. That is, \[ s - (t + u) = s - t - u. \]

Multiset.le_sub_add theorem

: s ≤ s - t + t

Full source

protected lemma le_sub_add : s ≤ s - t + t := Multiset.sub_le_iff_le_add.1 le_rfl

Submultiset Inequality: $s \leq s - t + t$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the multiset $s$ is a submultiset of the result of subtracting $t$ from $s$ and then adding $t$ back, i.e., $s \leq s - t + t$.

Multiset.le_add_sub theorem

: s ≤ t + (s - t)

Full source

protected lemma le_add_sub : s ≤ t + (s - t) := Multiset.sub_le_iff_le_add'.1 le_rfl

Submultiset Inequality: $s \leq t + (s - t)$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the multiset $s$ is a submultiset of the sum of $t$ and the difference $(s - t)$, i.e., $s \leq t + (s - t)$.

Multiset.sub_le_sub_right theorem

(hst : s ≤ t) : s - u ≤ t - u

Full source

protected lemma sub_le_sub_right (hst : s ≤ t) : s - u ≤ t - u :=
  Multiset.sub_le_iff_le_add'.mpr <| hst.trans Multiset.le_add_sub

Monotonicity of Multiset Subtraction: $s \leq t \Rightarrow s - u \leq t - u$

Informal description

For any multisets $s$, $t$, and $u$ over a type $\alpha$, if $s$ is a submultiset of $t$ (i.e., $s \leq t$), then the difference $s - u$ is a submultiset of the difference $t - u$ (i.e., $s - u \leq t - u$).

Multiset.add_sub_cancel_right theorem

: s + t - t = s

Full source

protected lemma add_sub_cancel_right : s + t - t = s := by ext a; simp

Right Cancellation Law for Multiset Addition and Subtraction: $(s + t) - t = s$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the subtraction of $t$ from the sum $s + t$ yields $s$, i.e., \[ (s + t) - t = s. \]

Multiset.cons_sub_of_le theorem

(a : α) {s t : Multiset α} (h : t ≤ s) : a ::ₘ s - t = a ::ₘ (s - t)

Full source

lemma cons_sub_of_le (a : α) {s t : Multiset α} (h : t ≤ s) : a ::ₘ s - t = a ::ₘ (s - t) := by
  rw [← singleton_add, ← singleton_add, Multiset.add_sub_assoc h]

Insertion and Subtraction Commute for Submultisets: $(a \mathbin{::} s) - t = a \mathbin{::} (s - t)$ when $t \leq s$

Informal description

For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$ such that $t$ is a submultiset of $s$ (i.e., $t \leq s$), the following equality holds: \[ (a \mathbin{::} s) - t = a \mathbin{::} (s - t), \] where $a \mathbin{::} s$ denotes the multiset obtained by adding one occurrence of $a$ to $s$.

Multiset.card_sub theorem

{s t : Multiset α} (h : t ≤ s) : card (s - t) = card s - card t

Full source

@[simp]
lemma card_sub {s t : Multiset α} (h : t ≤ s) : card (s - t) = card s - card t :=
  Nat.eq_sub_of_add_eq <| by rw [← card_add, Multiset.sub_add_cancel h]

Cardinality of Multiset Difference: $|s - t| = |s| - |t|$ when $t \leq s$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, if $t$ is a submultiset of $s$ (i.e., $t \leq s$), then the cardinality of the difference multiset $s - t$ is equal to the difference of the cardinalities of $s$ and $t$, i.e., $|s - t| = |s| - |t|$.

Multiset.sub_singleton theorem

(a : α) (s : Multiset α) : s - { a } = s.erase a

Full source

@[simp] theorem sub_singleton (a : α) (s : Multiset α) : s - {a} = s.erase a := by
  ext
  simp only [count_sub, count_singleton]
  split <;> simp_all

Difference with Singleton Equals Erasure: $s - \{a\} = \text{erase}(s, a)$

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the difference of $s$ and the singleton multiset $\{a\}$ is equal to the multiset obtained by erasing one occurrence of $a$ from $s$, i.e., $s - \{a\} = \text{erase}(s, a)$.

Multiset.mem_sub theorem

{a : α} {s t : Multiset α} : a ∈ s - t ↔ t.count a < s.count a

Full source

theorem mem_sub {a : α} {s t : Multiset α} :
    a ∈ s - ta ∈ s - t ↔ t.count a < s.count a := by
  rw [← count_pos, count_sub, Nat.sub_pos_iff_lt]

Membership in Multiset Difference via Multiplicity Comparison: $a \in s - t \leftrightarrow \text{count}_a t < \text{count}_a s$

Informal description

For any element $a$ of type $\alpha$ and any multisets $s$ and $t$ over $\alpha$, the element $a$ belongs to the difference multiset $s - t$ if and only if the multiplicity of $a$ in $t$ is strictly less than its multiplicity in $s$. That is, \[ a \in s - t \leftrightarrow \text{count}_a t < \text{count}_a s. \]

Multiset.Rel.add theorem

{s t u v} (hst : Rel r s t) (huv : Rel r u v) : Rel r (s + u) (t + v)

Full source

theorem Rel.add {s t u v} (hst : Rel r s t) (huv : Rel r u v) : Rel r (s + u) (t + v) := by
  induction hst with
  | zero => simpa using huv
  | cons hab hst ih => simpa using ih.cons hab

Preservation of Lifted Relation under Multiset Addition: $\text{Rel}\, r\, s\, t \land \text{Rel}\, r\, u\, v \to \text{Rel}\, r\, (s + u)\, (t + v)$

Informal description

Let $r$ be a relation between elements of types $\alpha$ and $\beta$. For any multisets $s, t$ over $\alpha$ and $u, v$ over $\beta$, if the relation $\text{Rel}\, r\, s\, t$ holds and the relation $\text{Rel}\, r\, u\, v$ holds, then the relation $\text{Rel}\, r\, (s + u)\, (t + v)$ also holds. Here, $\text{Rel}\, r$ denotes the lifting of the relation $r$ to multisets, and $+$ denotes the sum of multisets.

Multiset.rel_add_left theorem

 {as₀ as₁} : ∀ {bs}, Rel r (as₀ + as₁) bs ↔ ∃ bs₀ bs₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Full source

theorem rel_add_left {as₀ as₁} :
    ∀ {bs}, RelRel r (as₀ + as₁) bs ↔ ∃ bs₀ bs₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁ :=
  @(Multiset.induction_on as₀ (by simp) fun a s ih bs ↦ by
      simp only [ih, cons_add, rel_cons_left]
      constructor
      · intro h
        rcases h with ⟨b, bs', hab, h, rfl⟩
        rcases h with ⟨bs₀, bs₁, h₀, h₁, rfl⟩
        exact ⟨b ::ₘ bs₀, bs₁, ⟨b, bs₀, hab, h₀, rfl⟩, h₁, by simp⟩
      · intro h
        rcases h with ⟨bs₀, bs₁, h, h₁, rfl⟩
        rcases h with ⟨b, bs, hab, h₀, rfl⟩
        exact ⟨b, bs + bs₁, hab, ⟨bs, bs₁, h₀, h₁, rfl⟩, by simp⟩)

Lifting Relation to Multiset Addition: $\text{Rel}\, r\, (s + t)\, u \leftrightarrow \exists u₁ u₂, \text{Rel}\, r\, s\, u₁ ∧ \text{Rel}\, r\, t\, u₂ ∧ u = u₁ + u₂$

Informal description

For any relation $r$ between elements of types $\alpha$ and $\beta$, and for any multisets $as₀$, $as₁$ over $\alpha$ and $bs$ over $\beta$, the relation $\text{Rel}\, r\, (as₀ + as₁)\, bs$ holds if and only if there exist multisets $bs₀$, $bs₁$ over $\beta$ such that: 1. $\text{Rel}\, r\, as₀\, bs₀$ holds, 2. $\text{Rel}\, r\, as₁\, bs₁$ holds, and 3. $bs = bs₀ + bs₁$. Here, $\text{Rel}\, r\, s\, t$ means that there exists a bijection between the elements of $s$ and $t$ that respects the relation $r$.

Multiset.rel_add_right theorem

 {as bs₀ bs₁} : Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Full source

theorem rel_add_right {as bs₀ bs₁} :
    RelRel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁ := by
  rw [← rel_flip, rel_add_left]; simp [rel_flip]

Decomposition of Lifted Relation under Right Multiset Addition: $\text{Rel}\, r\, s\, (t + u) \leftrightarrow \exists s₁ s₂, \text{Rel}\, r\, s₁\, t ∧ \text{Rel}\, r\, s₂\, u ∧ s = s₁ + s₂$

Informal description

For any relation $r$ between elements of types $\alpha$ and $\beta$, and for any multisets $as$ over $\alpha$ and $bs₀, bs₁$ over $\beta$, the relation $\text{Rel}\, r\, as\, (bs₀ + bs₁)$ holds if and only if there exist multisets $as₀, as₁$ over $\alpha$ such that: 1. $\text{Rel}\, r\, as₀\, bs₀$ holds, 2. $\text{Rel}\, r\, as₁\, bs₁$ holds, and 3. $as = as₀ + as₁$. Here, $\text{Rel}\, r\, s\, t$ means that there exists a bijection between the elements of $s$ and $t$ that respects the relation $r$, and $+$ denotes the sum of multisets.

Multiset.nodup_singleton theorem

: ∀ a : α, Nodup ({ a } : Multiset α)

Full source

@[simp]
theorem nodup_singleton : ∀ a : α, Nodup ({a} : Multiset α) :=
  List.nodup_singleton

No-Duplicates Property of Singleton Multisets

Informal description

For any element $a$ of type $\alpha$, the singleton multiset $\{a\}$ has no duplicate elements.

Multiset.not_nodup_pair theorem

: ∀ a : α, ¬Nodup (a ::ₘ a ::ₘ 0)

Full source

theorem not_nodup_pair : ∀ a : α, ¬Nodup (a ::ₘ a ::ₘ 0) :=
  List.not_nodup_pair

Non-No-Duplicates Property for a Pair of Identical Elements in Multiset

Informal description

For any element $a$ of type $\alpha$, the multiset containing two copies of $a$ (i.e., $a ::ₘ a ::ₘ 0$) does not satisfy the `Nodup` property (i.e., it has duplicate elements).

Multiset.Nodup.erase theorem

[DecidableEq α] (a : α) {l} : Nodup l → Nodup (l.erase a)

Full source

theorem Nodup.erase [DecidableEq α] (a : α) {l} : Nodup l → Nodup (l.erase a) :=
  nodup_of_le (erase_le _ _)

Preservation of No-Duplicates Property under Multiset Erasure

Informal description

For any element $a$ in a type $\alpha$ with decidable equality, and for any multiset $l$ over $\alpha$ that has no duplicate elements, the multiset obtained by erasing one occurrence of $a$ from $l$ also has no duplicate elements.

Multiset.mem_sub_of_nodup theorem

[DecidableEq α] {a : α} {s t : Multiset α} (d : Nodup s) : a ∈ s - t ↔ a ∈ s ∧ a ∉ t

Full source

theorem mem_sub_of_nodup [DecidableEq α] {a : α} {s t : Multiset α} (d : Nodup s) :
    a ∈ s - ta ∈ s - t ↔ a ∈ s ∧ a ∉ t :=
  ⟨fun h =>
    ⟨mem_of_le (Multiset.sub_le_self ..) h, fun h' => by
      refine count_eq_zero.1 ?_ h
      rw [count_sub a s t, Nat.sub_eq_zero_iff_le]
      exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')⟩,
    fun ⟨h₁, h₂⟩ => Or.resolve_right (mem_add.1 <| mem_of_le Multiset.le_sub_add h₁) h₂⟩

Membership in Multiset Difference for Duplicate-Free Multisets: $a \in s - t \leftrightarrow (a \in s) \land (a \notin t)$

Informal description

For any element $a$ of type $\alpha$ with decidable equality and any multisets $s$ and $t$ over $\alpha$, if $s$ has no duplicate elements, then $a$ belongs to the difference multiset $s - t$ if and only if $a$ belongs to $s$ and $a$ does not belong to $t$. That is, \[ a \in s - t \leftrightarrow (a \in s) \land (a \notin t). \]

Notation (defined later)