Mathlib.Data.Multiset.Count

Multiset.countP definition

(s : Multiset α) : ℕ

Full source

/-- `countP p s` counts the number of elements of `s` (with multiplicity) that
  satisfy `p`. -/
def countP (s : Multiset α) : ℕ :=
  Quot.liftOn s (List.countP p) fun _l₁ _l₂ => Perm.countP_eq (p ·)

Count of elements satisfying a predicate in a multiset

Informal description

The function `countP p s` counts the number of elements (with multiplicity) in the multiset `s` that satisfy the predicate `p`.

Multiset.coe_countP theorem

(l : List α) : countP p l = l.countP p

Full source

@[simp]
theorem coe_countP (l : List α) : countP p l = l.countP p :=
  rfl

Equality of Counts Between List and Multiset for Predicate $p$

Informal description

For any list $l$ of elements of type $\alpha$, the count of elements (with multiplicity) in the multiset version of $l$ that satisfy predicate $p$ is equal to the count of elements in $l$ that satisfy $p$. That is, $\text{countP}_p(l) = l.\text{countP}_p$.

Multiset.countP_zero theorem

: countP p 0 = 0

Full source

@[simp]
theorem countP_zero : countP p 0 = 0 :=
  rfl

Count of Satisfying Elements in Empty Multiset is Zero

Informal description

For any predicate $p$, the count of elements satisfying $p$ in the empty multiset $0$ is $0$.

Multiset.countP_cons_of_pos theorem

{a : α} (s) : p a → countP p (a ::ₘ s) = countP p s + 1

Full source

@[simp]
theorem countP_cons_of_pos {a : α} (s) : p a → countP p (a ::ₘ s) = countP p s + 1 :=
  Quot.inductionOn s <| by simpa using fun _ => List.countP_cons_of_pos (p := (p ·))

Increment of Count When Inserting an Element Satisfying Predicate in Multiset

Informal description

For any element $a$ of type $\alpha$ and multiset $s$ over $\alpha$, if the predicate $p$ holds for $a$, then the count of elements satisfying $p$ in the multiset obtained by inserting $a$ into $s$ is equal to the count in $s$ plus one. That is, if $p(a)$ holds, then $\text{countP}_p(a ::ₘ s) = \text{countP}_p(s) + 1$.

Multiset.countP_cons_of_neg theorem

{a : α} (s) : ¬p a → countP p (a ::ₘ s) = countP p s

Full source

@[simp]
theorem countP_cons_of_neg {a : α} (s) : ¬p a → countP p (a ::ₘ s) = countP p s :=
  Quot.inductionOn s <| by simpa using fun _ => List.countP_cons_of_neg (p := (p ·))

Count Preservation in Multiset Insertion for Non-Satisfying Elements

Informal description

For any element $a$ of type $\alpha$ and multiset $s$ over $\alpha$, if the predicate $p$ does not hold for $a$ (i.e., $\neg p(a)$), then the count of elements satisfying $p$ in the multiset obtained by inserting $a$ into $s$ is equal to the count of elements satisfying $p$ in $s$ itself. That is, $\text{countP}_p(a \cons s) = \text{countP}_p(s)$ when $\neg p(a)$.

Multiset.countP_cons theorem

(b : α) (s) : countP p (b ::ₘ s) = countP p s + if p b then 1 else 0

Full source

theorem countP_cons (b : α) (s) : countP p (b ::ₘ s) = countP p s + if p b then 1 else 0 :=
  Quot.inductionOn s <| by simp [List.countP_cons]

Count Update When Adding Element to Multiset

Informal description

For any element $b$ of type $\alpha$ and any multiset $s$ over $\alpha$, the count of elements in $b ::ₘ s$ (the multiset obtained by adding $b$ to $s$) that satisfy predicate $p$ equals the count in $s$ plus $1$ if $p(b)$ holds, and plus $0$ otherwise. In other words: $$\text{countP}_p(b ::ₘ s) = \text{countP}_p(s) + \begin{cases} 1 & \text{if } p(b) \\ 0 & \text{otherwise} \end{cases}$$

Multiset.countP_le_card theorem

(s) : countP p s ≤ card s

Full source

theorem countP_le_card (s) : countP p s ≤ card s :=
  Quot.inductionOn s fun _l => countP_le_length (p := (p ·))

Count of Predicate-Satisfying Elements Bounded by Multiset Cardinality

Informal description

For any multiset $s$ and predicate $p$, the count of elements (with multiplicity) in $s$ satisfying $p$ is less than or equal to the cardinality of $s$, i.e., \[ \text{countP}_p(s) \leq |s|. \]

Multiset.card_eq_countP_add_countP theorem

(s) : card s = countP p s + countP (fun x => ¬p x) s

Full source

theorem card_eq_countP_add_countP (s) : card s = countP p s + countP (fun x => ¬p x) s :=
  Quot.inductionOn s fun l => by simp [l.length_eq_countP_add_countP p]

Cardinality Decomposition of a Multiset via Predicate Counts

Informal description

For any multiset $s$ and predicate $p$, the cardinality of $s$ is equal to the sum of the count of elements (with multiplicity) satisfying $p$ and the count of elements not satisfying $p$, i.e., $$|s| = \text{countP}\, p\, s + \text{countP}\, (\lambda x, \neg p\, x)\, s.$$

Multiset.countP_le_of_le theorem

{s t} (h : s ≤ t) : countP p s ≤ countP p t

Full source

@[gcongr]
theorem countP_le_of_le {s t} (h : s ≤ t) : countP p s ≤ countP p t :=
  leInductionOn h fun s => s.countP_le

Monotonicity of Count with Respect to Submultiset Inclusion

Informal description

For any multisets $s$ and $t$ such that $s \leq t$ (i.e., $s$ is a submultiset of $t$), and for any predicate $p$, the count of elements in $s$ satisfying $p$ is less than or equal to the count of elements in $t$ satisfying $p$. In other words, if $s \leq t$, then $\text{countP}(p, s) \leq \text{countP}(p, t)$.

Multiset.countP_True theorem

{s : Multiset α} : countP (fun _ => True) s = card s

Full source

@[simp]
theorem countP_True {s : Multiset α} : countP (fun _ => True) s = card s :=
  Quot.inductionOn s fun _l => congrFun List.countP_true _

Count of All Elements Equals Cardinality in Multiset

Informal description

For any multiset $s$ over a type $\alpha$, the count of elements satisfying the always-true predicate (i.e., counting all elements with multiplicity) equals the cardinality of $s$, i.e., $\mathrm{countP}\, (\lambda \_. \mathrm{True})\, s = \mathrm{card}\, s$.

Multiset.countP_False theorem

{s : Multiset α} : countP (fun _ => False) s = 0

Full source

@[simp]
theorem countP_False {s : Multiset α} : countP (fun _ => False) s = 0 :=
  Quot.inductionOn s fun _l => congrFun List.countP_false _

Count of False Predicate in Multiset is Zero

Informal description

For any multiset $s$ over a type $\alpha$, the count of elements satisfying the always-false predicate is zero, i.e., $\text{countP}(\lambda \_. \text{False}, s) = 0$.

Multiset.countP_attach theorem

(s : Multiset α) : s.attach.countP (fun a : { a // a ∈ s } ↦ p a) = s.countP p

Full source

lemma countP_attach (s : Multiset α) : s.attach.countP (fun a : {a // a ∈ s} ↦ p a) = s.countP p :=
  Quotient.inductionOn s fun l => by
    simp only [quot_mk_to_coe, coe_countP, coe_attach, coe_countP, ← List.countP_attach (l := l)]
    rfl

Count Preservation in Attached Multiset: $\mathrm{countP}(p, s.\mathrm{attach}) = \mathrm{countP}(p, s)$

Informal description

For any multiset $s$ and predicate $p$, the count of elements in the attached multiset $\{a \mid a \in s\}$ that satisfy $p$ is equal to the count of elements in $s$ that satisfy $p$.

Multiset.countP_pos theorem

{s} : 0 < countP p s ↔ ∃ a ∈ s, p a

Full source

theorem countP_pos {s} : 0 < countP p s ↔ ∃ a ∈ s, p a :=
  Quot.inductionOn s fun _l => by simp

Positivity of Count in Multiset

Informal description

For a multiset $s$ and a predicate $p$, the count of elements in $s$ (with multiplicity) satisfying $p$ is positive if and only if there exists an element $a$ in $s$ such that $p(a)$ holds. In other words, $0 < \text{countP}(p, s) \leftrightarrow \exists a \in s, p(a)$.

Multiset.countP_eq_zero theorem

{s} : countP p s = 0 ↔ ∀ a ∈ s, ¬p a

Full source

theorem countP_eq_zero {s} : countPcountP p s = 0 ↔ ∀ a ∈ s, ¬p a :=
  Quot.inductionOn s fun _l => by simp [List.countP_eq_zero]

Count of Predicate-Satisfying Elements is Zero if and only if No Element Satisfies Predicate

Informal description

For a multiset $s$, the count of elements (with multiplicity) satisfying a predicate $p$ is zero if and only if no element in $s$ satisfies $p$. In other words, $\text{countP}(p, s) = 0 \leftrightarrow \forall a \in s, \neg p(a)$.

Multiset.countP_eq_card theorem

{s} : countP p s = card s ↔ ∀ a ∈ s, p a

Full source

theorem countP_eq_card {s} : countPcountP p s = card s ↔ ∀ a ∈ s, p a :=
  Quot.inductionOn s fun _l => by simp [List.countP_eq_length]

Count of Predicate-Satisfying Elements Equals Cardinality if and Only if All Elements Satisfy Predicate

Informal description

For a multiset $s$ and a predicate $p$, the count of elements in $s$ (with multiplicity) satisfying $p$ equals the cardinality of $s$ if and only if every element in $s$ satisfies $p$. In other words, $\mathrm{countP}\, p\, s = \mathrm{card}\, s \leftrightarrow \forall a \in s, p(a)$.

Multiset.countP_pos_of_mem theorem

{s a} (h : a ∈ s) (pa : p a) : 0 < countP p s

Full source

theorem countP_pos_of_mem {s a} (h : a ∈ s) (pa : p a) : 0 < countP p s :=
  countP_pos.2 ⟨_, h, pa⟩

Positivity of Count for Predicate-Satisfying Element in Multiset

Informal description

For any multiset $s$ and element $a \in s$, if the predicate $p$ holds for $a$, then the count of elements in $s$ (with multiplicity) satisfying $p$ is positive, i.e., $0 < \text{countP}(p, s)$.

Multiset.countP_congr theorem

 {s s' : Multiset α} (hs : s = s') {p p' : α → Prop} [DecidablePred p] [DecidablePred p'] (hp : ∀ x ∈ s, p x = p' x) :
  s.countP p = s'.countP p'

Full source

@[congr]
theorem countP_congr {s s' : Multiset α} (hs : s = s')
    {p p' : α → Prop} [DecidablePred p] [DecidablePred p']
    (hp : ∀ x ∈ s, p x = p' x) : s.countP p = s'.countP p' := by
  revert hs hp
  exact Quot.induction_on₂ s s'
    (fun l l' hs hp => by
      simp only [quot_mk_to_coe'', coe_eq_coe] at hs
      apply hs.countP_congr
      simpa using hp)

Count of Predicate-Satisfying Elements is Preserved Under Predicate Agreement and Multiset Equality

Informal description

Let $s$ and $s'$ be multisets of type $\alpha$ such that $s = s'$, and let $p$ and $p'$ be predicates on $\alpha$ with decidable instances. If for every element $x \in s$, the predicates $p$ and $p'$ agree (i.e., $p(x) = p'(x)$), then the count of elements in $s$ satisfying $p$ is equal to the count of elements in $s'$ satisfying $p'$.

Multiset.count definition

(a : α) : Multiset α → ℕ

Full source

/-- `count a s` is the multiplicity of `a` in `s`. -/
def count (a : α) : Multiset α → ℕ :=
  countP (a = ·)

Multiplicity of an element in a multiset

Informal description

The function `count a s` returns the multiplicity of the element `a` in the multiset `s`, i.e., the number of times `a` appears in `s` (counting multiplicities).

Multiset.coe_count theorem

(a : α) (l : List α) : count a (ofList l) = l.count a

Full source

@[simp]
theorem coe_count (a : α) (l : List α) : count a (ofList l) = l.count a := by
  simp_rw [count, List.count, coe_countP (a = ·) l, @eq_comm _ a]
  rfl

Multiset-List Count Correspondence: $\text{count } a (\text{ofList } l) = l.\text{count } a$

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of type $\alpha$, the multiplicity of $a$ in the multiset constructed from $l$ (denoted $\text{ofList } l$) is equal to the count of $a$ in the list $l$. That is, $\text{count } a (\text{ofList } l) = l.\text{count } a$.

Multiset.count_zero theorem

(a : α) : count a 0 = 0

Full source

@[simp]
theorem count_zero (a : α) : count a 0 = 0 :=
  rfl

Multiplicity of an Element in the Empty Multiset is Zero

Informal description

For any element $a$ of type $\alpha$, the multiplicity of $a$ in the empty multiset is zero, i.e., $\text{count}_a(0) = 0$.

Multiset.count_cons_self theorem

(a : α) (s : Multiset α) : count a (a ::ₘ s) = count a s + 1

Full source

@[simp]
theorem count_cons_self (a : α) (s : Multiset α) : count a (a ::ₘ s) = count a s + 1 :=
  countP_cons_of_pos _ <| rfl

Increment of Multiplicity When Inserting an Element in Multiset

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the multiplicity of $a$ in the multiset obtained by inserting $a$ into $s$ is equal to the multiplicity of $a$ in $s$ plus one, i.e., $\text{count}_a(a ::ₘ s) = \text{count}_a(s) + 1$.

Multiset.count_cons_of_ne theorem

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

Full source

@[simp]
theorem count_cons_of_ne {a b : α} (h : a ≠ b) (s : Multiset α) : count a (b ::ₘ s) = count a s :=
  countP_cons_of_neg _ <| h

Multiplicity Preservation in Multiset Insertion for Distinct Elements

Informal description

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

Multiset.count_le_card theorem

(a : α) (s) : count a s ≤ card s

Full source

theorem count_le_card (a : α) (s) : count a s ≤ card s :=
  countP_le_card _ _

Multiplicity Bounded by Multiset Cardinality

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the multiplicity of $a$ in $s$ is less than or equal to the cardinality of $s$, i.e., $\text{count}_a(s) \leq |s|$.

Multiset.count_le_of_le theorem

(a : α) {s t} : s ≤ t → count a s ≤ count a t

Full source

@[gcongr]
theorem count_le_of_le (a : α) {s t} : s ≤ t → count a s ≤ count a t :=
  countP_le_of_le _

Monotonicity of Element Count with Respect to Submultiset Inclusion

Informal description

For any element $a$ of type $\alpha$ and any multisets $s$ and $t$ of type $\alpha$ such that $s \leq t$ (i.e., $s$ is a submultiset of $t$), the multiplicity of $a$ in $s$ is less than or equal to its multiplicity in $t$. In other words, if $s \leq t$, then $\text{count}(a, s) \leq \text{count}(a, t)$.

Multiset.count_le_count_cons theorem

(a b : α) (s : Multiset α) : count a s ≤ count a (b ::ₘ s)

Full source

theorem count_le_count_cons (a b : α) (s : Multiset α) : count a s ≤ count a (b ::ₘ s) :=
  count_le_of_le _ (le_cons_self _ _)

Monotonicity of Element Count Under Multiset Insertion

Informal description

For any elements $a, b$ of type $\alpha$ and any multiset $s$ over $\alpha$, the multiplicity of $a$ in $s$ is less than or equal to its multiplicity in the multiset obtained by adding $b$ to $s$, i.e., $\text{count}(a, s) \leq \text{count}(a, b ::ₘ s)$.

Multiset.count_cons theorem

(a b : α) (s : Multiset α) : count a (b ::ₘ s) = count a s + if a = b then 1 else 0

Full source

theorem count_cons (a b : α) (s : Multiset α) :
    count a (b ::ₘ s) = count a s + if a = b then 1 else 0 :=
  countP_cons (a = ·) _ _

Multiplicity Update When Adding Element to Multiset: $\text{count}(a, b ::ₘ s) = \text{count}(a, s) + \mathbb{1}_{a = b}$

Informal description

For any elements $a, b$ of type $\alpha$ and any multiset $s$ over $\alpha$, the multiplicity of $a$ in the multiset obtained by adding $b$ to $s$ is equal to the multiplicity of $a$ in $s$ plus $1$ if $a = b$, and plus $0$ otherwise. In other words: $$\text{count}(a, b ::ₘ s) = \text{count}(a, s) + \begin{cases} 1 & \text{if } a = b \\ 0 & \text{otherwise} \end{cases}$$

Multiset.count_singleton_self theorem

(a : α) : count a ({ a } : Multiset α) = 1

Full source

theorem count_singleton_self (a : α) : count a ({a} : Multiset α) = 1 :=
  count_eq_one_of_mem (nodup_singleton a) <| mem_singleton_self a

Multiplicity of Element in Own Singleton Multiset: $\text{count}(a, \{a\}) = 1$

Informal description

For any element $a$ of type $\alpha$, the multiplicity of $a$ in the singleton multiset $\{a\}$ is equal to $1$.

Multiset.count_singleton theorem

(a b : α) : count a ({ b } : Multiset α) = if a = b then 1 else 0

Full source

theorem count_singleton (a b : α) : count a ({b} : Multiset α) = if a = b then 1 else 0 := by
  simp only [count_cons, ← cons_zero, count_zero, Nat.zero_add]

Multiplicity in Singleton Multiset: $\text{count}(a, \{b\}) = \mathbb{1}_{a = b}$

Informal description

For any elements $a$ and $b$ of type $\alpha$, the multiplicity of $a$ in the singleton multiset $\{b\}$ is $1$ if $a = b$ and $0$ otherwise. In other words: $$\text{count}(a, \{b\}) = \begin{cases} 1 & \text{if } a = b \\ 0 & \text{otherwise} \end{cases}$$

Multiset.count_attach theorem

(a : { x // x ∈ s }) : s.attach.count a = s.count ↑a

Full source

@[simp]
lemma count_attach (a : {x // x ∈ s}) : s.attach.count a = s.count ↑a :=
  Eq.trans (countP_congr rfl fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _

Count Preservation in Attached Multiset: $\mathrm{count}(a, s.\mathrm{attach}) = \mathrm{count}(\uparrow a, s)$

Informal description

For any element $a$ in the attached multiset $\{x \mid x \in s\}$, the count of $a$ in $s.\mathrm{attach}$ is equal to the count of the underlying element $\uparrow a$ in the original multiset $s$.

Multiset.count_pos theorem

{a : α} {s : Multiset α} : 0 < count a s ↔ a ∈ s

Full source

theorem count_pos {a : α} {s : Multiset α} : 0 < count a s ↔ a ∈ s := by simp [count, countP_pos]

Positive Count Characterizes Membership in Multiset: $0 < \mathrm{count}(a, s) \leftrightarrow a \in s$

Informal description

For any element $a$ and multiset $s$, the multiplicity of $a$ in $s$ is positive (i.e., $0 < \mathrm{count}(a, s)$) if and only if $a$ is an element of $s$ (i.e., $a \in s$).

Multiset.one_le_count_iff_mem theorem

{a : α} {s : Multiset α} : 1 ≤ count a s ↔ a ∈ s

Full source

theorem one_le_count_iff_mem {a : α} {s : Multiset α} : 1 ≤ count a s ↔ a ∈ s := by
  rw [succ_le_iff, count_pos]

Membership Criterion via Count: $1 \leq \mathrm{count}(a, s) \leftrightarrow a \in s$

Informal description

For any element $a$ and multiset $s$, the multiplicity of $a$ in $s$ is at least one (i.e., $1 \leq \mathrm{count}(a, s)$) if and only if $a$ is an element of $s$ (i.e., $a \in s$).

Multiset.count_eq_zero_of_not_mem theorem

{a : α} {s : Multiset α} (h : a ∉ s) : count a s = 0

Full source

@[simp]
theorem count_eq_zero_of_not_mem {a : α} {s : Multiset α} (h : a ∉ s) : count a s = 0 :=
  by_contradiction fun h' => h <| count_pos.1 (Nat.pos_of_ne_zero h')

Zero Count for Non-Members in Multiset: $\mathrm{count}(a, s) = 0$ when $a \notin s$

Informal description

For any element $a$ and multiset $s$, if $a$ is not an element of $s$ (i.e., $a \notin s$), then the multiplicity of $a$ in $s$ is zero (i.e., $\mathrm{count}(a, s) = 0$).

Multiset.count_ne_zero theorem

{a : α} : count a s ≠ 0 ↔ a ∈ s

Full source

lemma count_ne_zero {a : α} : countcount a s ≠ 0count a s ≠ 0 ↔ a ∈ s := Nat.pos_iff_ne_zero.symm.trans count_pos

Nonzero Count Characterizes Membership in Multiset: $\mathrm{count}(a, s) \neq 0 \leftrightarrow a \in s$

Informal description

For any element $a$ and multiset $s$, the multiplicity of $a$ in $s$ is nonzero (i.e., $\mathrm{count}(a, s) \neq 0$) if and only if $a$ is an element of $s$ (i.e., $a \in s$).

Multiset.count_eq_zero theorem

{a : α} : count a s = 0 ↔ a ∉ s

Full source

@[simp] lemma count_eq_zero {a : α} : countcount a s = 0 ↔ a ∉ s := count_ne_zero.not_right

Zero Count Characterizes Non-Membership in Multiset: $\mathrm{count}(a, s) = 0 \leftrightarrow a \notin s$

Informal description

For any element $a$ in a multiset $s$, the multiplicity of $a$ in $s$ is zero if and only if $a$ is not an element of $s$. That is, $\mathrm{count}(a, s) = 0 \leftrightarrow a \notin s$.

Multiset.count_eq_card theorem

{a : α} {s} : count a s = card s ↔ ∀ x ∈ s, a = x

Full source

theorem count_eq_card {a : α} {s} : countcount a s = card s ↔ ∀ x ∈ s, a = x := by
  simp [countP_eq_card, count, @eq_comm _ a]

Characterization of Uniform Multisets: $\text{count}(a, s) = \text{card}(s) \leftrightarrow s$ consists entirely of $a$

Informal description

For any element $a$ in a multiset $s$, the multiplicity of $a$ in $s$ equals the cardinality of $s$ if and only if every element in $s$ is equal to $a$. In other words, $\text{count}(a, s) = \text{card}(s) \leftrightarrow (\forall x \in s, x = a)$.

Multiset.ext theorem

{s t : Multiset α} : s = t ↔ ∀ a, count a s = count a t

Full source

theorem ext {s t : Multiset α} : s = t ↔ ∀ a, count a s = count a t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ => Quotient.eq.trans <| by
    simp only [quot_mk_to_coe, mem_coe, coe_count, decide_eq_true_eq]
    apply perm_iff_count

Multiset Equality via Element Multiplicity

Informal description

Two multisets $s$ and $t$ are equal if and only if for every element $a$, the multiplicity of $a$ in $s$ is equal to the multiplicity of $a$ in $t$. That is, $s = t \leftrightarrow \forall a, \text{count}(a, s) = \text{count}(a, t)$.

Multiset.ext' theorem

{s t : Multiset α} : (∀ a, count a s = count a t) → s = t

Full source

@[ext]
theorem ext' {s t : Multiset α} : (∀ a, count a s = count a t) → s = t :=
  ext.2

Multiset Equality via Equal Multiplicities

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, if the multiplicity of every element $a$ in $s$ is equal to its multiplicity in $t$, then $s$ and $t$ are equal. That is, $(\forall a, \text{count}(a, s) = \text{count}(a, t)) \rightarrow s = t$.

Multiset.count_injective theorem

: Injective fun (s : Multiset α) a ↦ s.count a

Full source

lemma count_injective : Injective fun (s : Multiset α) a ↦ s.count a :=
  fun _s _t hst ↦ ext' <| congr_fun hst

Injectivity of Multiset Multiplicity Counting Function

Informal description

The function that maps a multiset $s$ over a type $\alpha$ to the function counting multiplicities of elements in $s$ is injective. In other words, if two multisets $s$ and $t$ satisfy $\text{count}(a, s) = \text{count}(a, t)$ for all elements $a \in \alpha$, then $s = t$.

Multiset.le_iff_count theorem

{s t : Multiset α} : s ≤ t ↔ ∀ a, count a s ≤ count a t

Full source

theorem le_iff_count {s t : Multiset α} : s ≤ t ↔ ∀ a, count a s ≤ count a t :=
  Quotient.inductionOn₂ s t fun _ _ ↦ by simp [subperm_iff_count]

Multiset Inclusion Criterion via Element Multiplicity

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the multiset inclusion $s \leq t$ holds if and only if for every element $a \in \alpha$, the multiplicity of $a$ in $s$ is less than or equal to its multiplicity in $t$. That is, $s \leq t \leftrightarrow \forall a, \text{count } a s \leq \text{count } a t$.

Multiset.Rel.countP_eq theorem

 (r : α → α → Prop) [IsTrans α r] [IsSymm α r] {s t : Multiset α} (x : α) [DecidablePred (r x)] (h : Rel r s t) :
  countP (r x) s = countP (r x) t

Full source

theorem Rel.countP_eq (r : α → α → Prop) [IsTrans α r] [IsSymm α r] {s t : Multiset α} (x : α)
    [DecidablePred (r x)] (h : Rel r s t) : countP (r x) s = countP (r x) t := by
  induction s using Multiset.induction_on generalizing t with
  | empty => rw [rel_zero_left.mp h]
  | cons y s ih =>
    obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h
    rw [countP_cons, countP_cons, ih hb2]
    simp only [decide_eq_true_eq, Nat.add_right_inj]
    exact (if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)

Preservation of Related Element Counts in Multisets under Symmetric and Transitive Relations

Informal description

Let $r$ be a symmetric and transitive relation on a type $\alpha$, and let $s$ and $t$ be multisets over $\alpha$ such that $\text{Rel}\,r\,s\,t$ holds. Then for any element $x \in \alpha$, the number of elements in $s$ related to $x$ by $r$ is equal to the number of elements in $t$ related to $x$ by $r$. That is, $$\text{countP}\,(r\,x)\,s = \text{countP}\,(r\,x)\,t.$$

Multiset.nodup_iff_count_le_one theorem

[DecidableEq α] {s : Multiset α} : Nodup s ↔ ∀ a, count a s ≤ 1

Full source

theorem nodup_iff_count_le_one [DecidableEq α] {s : Multiset α} : NodupNodup s ↔ ∀ a, count a s ≤ 1 :=
  Quot.induction_on s fun _l => by
    simp only [quot_mk_to_coe'', coe_nodup, mem_coe, coe_count]
    exact List.nodup_iff_count_le_one

Characterization of Duplicate-Free Multisets via Element Multiplicity

Informal description

A multiset $s$ over a type $\alpha$ with decidable equality has no duplicate elements if and only if every element $a \in \alpha$ appears in $s$ with multiplicity at most 1. That is, $\text{Nodup } s \leftrightarrow \forall a, \text{count } a s \leq 1$.

Multiset.nodup_iff_count_eq_one theorem

[DecidableEq α] : Nodup s ↔ ∀ a ∈ s, count a s = 1

Full source

theorem nodup_iff_count_eq_one [DecidableEq α] : NodupNodup s ↔ ∀ a ∈ s, count a s = 1 :=
  Quot.induction_on s fun _l => by simpa using List.nodup_iff_count_eq_one

Characterization of Duplicate-Free Multisets via Exact Multiplicity

Informal description

For a multiset $s$ over a type $\alpha$ with decidable equality, $s$ has no duplicate elements if and only if every element $a$ in $s$ has multiplicity exactly 1. That is, $\text{Nodup } s \leftrightarrow \forall a \in s, \text{count } a s = 1$.

Multiset.count_eq_one_of_mem theorem

[DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) (h : a ∈ s) : count a s = 1

Full source

@[simp]
theorem count_eq_one_of_mem [DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) (h : a ∈ s) :
    count a s = 1 :=
  nodup_iff_count_eq_one.mp d a h

Multiplicity of Elements in Duplicate-Free Multisets is One

Informal description

For a multiset $s$ over a type $\alpha$ with decidable equality, if $s$ has no duplicate elements and an element $a$ is a member of $s$, then the multiplicity of $a$ in $s$ is exactly 1. That is, if $\text{Nodup } s$ and $a \in s$, then $\text{count } a s = 1$.

Multiset.count_eq_of_nodup theorem

[DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) : count a s = if a ∈ s then 1 else 0

Full source

theorem count_eq_of_nodup [DecidableEq α] {a : α} {s : Multiset α} (d : Nodup s) :
    count a s = if a ∈ s then 1 else 0 := by
  split_ifs with h
  · exact count_eq_one_of_mem d h
  · exact count_eq_zero_of_not_mem h

Multiplicity in Duplicate-Free Multisets: $\mathrm{count}(a, s) = \mathbb{1}_{a \in s}$

Informal description

For a multiset $s$ over a type $\alpha$ with decidable equality, if $s$ has no duplicate elements, then the multiplicity of an element $a$ in $s$ is $1$ if $a \in s$ and $0$ otherwise. That is, $\mathrm{count}(a, s) = \begin{cases} 1 & \text{if } a \in s \\ 0 & \text{otherwise} \end{cases}$.