Mathlib.Data.Multiset.Dedup

Multiset.dedup definition

(s : Multiset α) : Multiset α

Full source

/-- `dedup s` removes duplicates from `s`, yielding a `nodup` multiset. -/
def dedup (s : Multiset α) : Multiset α :=
  Quot.liftOn s (fun l => (l.dedup : Multiset α)) fun _ _ p => Quot.sound p.dedup

Remove duplicates from a multiset

Informal description

The function `dedup` takes a multiset `s` and returns a multiset with duplicate elements removed, ensuring the result has no duplicates (`nodup`).

Multiset.coe_dedup theorem

(l : List α) : @dedup α _ l = l.dedup

Full source

@[simp]
theorem coe_dedup (l : List α) : @dedup α _ l = l.dedup :=
  rfl

Equality of List and Multiset Deduplication: $\text{dedup}(l) = \text{dedup}(\text{to\_multiset}(l))$

Informal description

For any list $l$ of elements of type $\alpha$, the multiset obtained by removing duplicates from $l$ (via the `dedup` function) is equal to the multiset obtained by first converting $l$ to a multiset and then removing duplicates.

Multiset.dedup_zero theorem

: @dedup α _ 0 = 0

Full source

@[simp]
theorem dedup_zero : @dedup α _ 0 = 0 :=
  rfl

Deduplication of Empty Multiset is Empty

Informal description

The deduplication of the empty multiset $0$ is equal to $0$ itself, i.e., $\mathrm{dedup}(0) = 0$.

Multiset.mem_dedup theorem

{a : α} {s : Multiset α} : a ∈ dedup s ↔ a ∈ s

Full source

@[simp]
theorem mem_dedup {a : α} {s : Multiset α} : a ∈ dedup sa ∈ dedup s ↔ a ∈ s :=
  Quot.induction_on s fun _ => List.mem_dedup

Membership in Deduplicated Multiset Equals Membership in Original

Informal description

For any element $a$ and multiset $s$, the element $a$ belongs to the deduplicated multiset $\mathrm{dedup}(s)$ if and only if $a$ belongs to $s$.

Multiset.dedup_cons_of_mem theorem

{a : α} {s : Multiset α} : a ∈ s → dedup (a ::ₘ s) = dedup s

Full source

@[simp]
theorem dedup_cons_of_mem {a : α} {s : Multiset α} : a ∈ s → dedup (a ::ₘ s) = dedup s :=
  Quot.induction_on s fun _ m => @congr_arg _ _ _ _ ofList <| List.dedup_cons_of_mem m

Deduplication of Multiset Insertion When Element Already Present

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ is an element of $s$, then the deduplication of the multiset obtained by inserting $a$ into $s$ is equal to the deduplication of $s$ itself. In other words, if $a \in s$, then $\text{dedup}(a \cons s) = \text{dedup}(s)$.

Multiset.dedup_cons_of_not_mem theorem

{a : α} {s : Multiset α} : a ∉ s → dedup (a ::ₘ s) = a ::ₘ dedup s

Full source

@[simp]
theorem dedup_cons_of_not_mem {a : α} {s : Multiset α} : a ∉ s → dedup (a ::ₘ s) = a ::ₘ dedup s :=
  Quot.induction_on s fun _ m => congr_arg ofList <| List.dedup_cons_of_not_mem m

Deduplication of Multiset Insertion When Element Not Present

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ is not in $s$, then the deduplication of the multiset obtained by inserting $a$ into $s$ is equal to the multiset obtained by inserting $a$ into the deduplication of $s$. In symbols: \[ a \notin s \implies \text{dedup}(a \cons s) = a \cons \text{dedup}(s). \]

Multiset.dedup_le theorem

(s : Multiset α) : dedup s ≤ s

Full source

theorem dedup_le (s : Multiset α) : dedup s ≤ s :=
  Quot.induction_on s fun _ => (dedup_sublist _).subperm

Deduplication Yields Submultiset: $\operatorname{dedup}(s) \leq s$

Informal description

For any multiset $s$, the deduplicated multiset $\operatorname{dedup}(s)$ is a submultiset of $s$, i.e., $\operatorname{dedup}(s) \leq s$.

Multiset.dedup_subset theorem

(s : Multiset α) : dedup s ⊆ s

Full source

theorem dedup_subset (s : Multiset α) : dedupdedup s ⊆ s :=
  subset_of_le <| dedup_le _

Deduplication Yields Subset: $\operatorname{dedup}(s) \subseteq s$

Informal description

For any multiset $s$, the deduplicated multiset $\operatorname{dedup}(s)$ is a subset of $s$, i.e., $\operatorname{dedup}(s) \subseteq s$.

Multiset.subset_dedup theorem

(s : Multiset α) : s ⊆ dedup s

Full source

theorem subset_dedup (s : Multiset α) : s ⊆ dedup s := fun _ => mem_dedup.2

Subset Property of Deduplication: $s \subseteq \mathrm{dedup}(s)$

Informal description

For any multiset $s$, $s$ is a subset of its deduplicated version $\mathrm{dedup}(s)$.

Multiset.dedup_subset' theorem

{s t : Multiset α} : dedup s ⊆ t ↔ s ⊆ t

Full source

@[simp]
theorem dedup_subset' {s t : Multiset α} : dedupdedup s ⊆ tdedup s ⊆ t ↔ s ⊆ t :=
  ⟨Subset.trans (subset_dedup _), Subset.trans (dedup_subset _)⟩

Deduplication Subset Equivalence: $\operatorname{dedup}(s) \subseteq t \leftrightarrow s \subseteq t$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the deduplicated multiset $\operatorname{dedup}(s)$ is a subset of $t$ if and only if $s$ is a subset of $t$.

Multiset.subset_dedup' theorem

{s t : Multiset α} : s ⊆ dedup t ↔ s ⊆ t

Full source

@[simp]
theorem subset_dedup' {s t : Multiset α} : s ⊆ dedup ts ⊆ dedup t ↔ s ⊆ t :=
  ⟨fun h => Subset.trans h (dedup_subset _), fun h => Subset.trans h (subset_dedup _)⟩

Subset Equivalence for Deduplication: $s \subseteq \operatorname{dedup}(t) \leftrightarrow s \subseteq t$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, $s$ is a subset of the deduplicated multiset $\operatorname{dedup}(t)$ if and only if $s$ is a subset of $t$.

Multiset.nodup_dedup theorem

(s : Multiset α) : Nodup (dedup s)

Full source

@[simp]
theorem nodup_dedup (s : Multiset α) : Nodup (dedup s) :=
  Quot.induction_on s List.nodup_dedup

Deduplicated multiset has no duplicates

Informal description

For any multiset $s$ over a type $\alpha$, the deduplicated multiset $\operatorname{dedup}(s)$ has no duplicate elements.

Multiset.dedup_eq_self theorem

{s : Multiset α} : dedup s = s ↔ Nodup s

Full source

theorem dedup_eq_self {s : Multiset α} : dedupdedup s = s ↔ Nodup s :=
  ⟨fun e => e ▸ nodup_dedup s, Quot.induction_on s fun _ h => congr_arg ofList h.dedup⟩

Deduplication Equals Original Multiset if and only if No Duplicates

Informal description

For any multiset $s$ over a type $\alpha$, the deduplication of $s$ equals $s$ if and only if $s$ has no duplicate elements, i.e., $\operatorname{dedup}(s) = s \leftrightarrow \operatorname{Nodup}(s)$.

Multiset.count_dedup theorem

(m : Multiset α) (a : α) : m.dedup.count a = if a ∈ m then 1 else 0

Full source

theorem count_dedup (m : Multiset α) (a : α) : m.dedup.count a = if a ∈ m then 1 else 0 :=
  Quot.induction_on m fun _ => by
    simp only [quot_mk_to_coe'', coe_dedup, mem_coe, List.mem_dedup, coe_nodup, coe_count]
    apply List.count_dedup _ _

Multiplicity in Deduplicated Multiset: $\operatorname{count}_a(\operatorname{dedup}(m)) = \mathbb{1}_{a \in m}$

Informal description

For any multiset $m$ over a type $\alpha$ and any element $a$ of type $\alpha$, the multiplicity of $a$ in the deduplicated multiset $\operatorname{dedup}(m)$ is equal to $1$ if $a$ is present in $m$ and $0$ otherwise. That is, $\operatorname{count}_a(\operatorname{dedup}(m)) = \begin{cases} 1 & \text{if } a \in m \\ 0 & \text{otherwise} \end{cases}$.

Multiset.dedup_idem theorem

{m : Multiset α} : m.dedup.dedup = m.dedup

Full source

@[simp]
theorem dedup_idem {m : Multiset α} : m.dedup.dedup = m.dedup :=
  Quot.induction_on m fun _ => @congr_arg _ _ _ _ ofList List.dedup_idem

Idempotence of Multiset Deduplication

Informal description

For any multiset $m$, applying the deduplication operation twice is equivalent to applying it once, i.e., $\text{dedup}(\text{dedup}(m)) = \text{dedup}(m)$.

Multiset.dedup_eq_zero theorem

{s : Multiset α} : dedup s = 0 ↔ s = 0

Full source

theorem dedup_eq_zero {s : Multiset α} : dedupdedup s = 0 ↔ s = 0 :=
  ⟨fun h => eq_zero_of_subset_zero <| h ▸ subset_dedup _, fun h => h.symm ▸ dedup_zero⟩

Deduplication Yields Empty Multiset if and only if Original is Empty

Informal description

For any multiset $s$, the deduplication of $s$ is equal to the empty multiset $0$ if and only if $s$ itself is equal to $0$, i.e., $\mathrm{dedup}(s) = 0 \leftrightarrow s = 0$.

Multiset.dedup_singleton theorem

{a : α} : dedup ({ a } : Multiset α) = { a }

Full source

@[simp]
theorem dedup_singleton {a : α} : dedup ({a} : Multiset α) = {a} :=
  (nodup_singleton _).dedup

Deduplication Preserves Singleton Multisets

Informal description

For any element $a$ of type $\alpha$, the deduplication of the singleton multiset $\{a\}$ is equal to itself, i.e., $\mathrm{dedup}(\{a\}) = \{a\}$.

Multiset.le_dedup theorem

{s t : Multiset α} : s ≤ dedup t ↔ s ≤ t ∧ Nodup s

Full source

theorem le_dedup {s t : Multiset α} : s ≤ dedup t ↔ s ≤ t ∧ Nodup s :=
  ⟨fun h => ⟨le_trans h (dedup_le _), nodup_of_le h (nodup_dedup _)⟩,
   fun ⟨l, d⟩ => (le_iff_subset d).2 <| Subset.trans (subset_of_le l) (subset_dedup _)⟩

Submultiset Relation to Deduplication: $s \leq \operatorname{dedup}(t) \leftrightarrow s \leq t \land \operatorname{Nodup}(s)$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, the relation $s \leq \operatorname{dedup}(t)$ holds if and only if $s \leq t$ and $s$ has no duplicate elements.

Multiset.le_dedup_self theorem

{s : Multiset α} : s ≤ dedup s ↔ Nodup s

Full source

theorem le_dedup_self {s : Multiset α} : s ≤ dedup s ↔ Nodup s := by
  rw [le_dedup, and_iff_right le_rfl]

Submultiset of Deduplication Equals Original if and only if No Duplicates

Informal description

For any multiset $s$ over a type $\alpha$, the relation $s \leq \operatorname{dedup}(s)$ holds if and only if $s$ has no duplicate elements.

Multiset.dedup_ext theorem

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

Full source

theorem dedup_ext {s t : Multiset α} : dedupdedup s = dedup t ↔ ∀ a, a ∈ s ↔ a ∈ t := by
  simp [Nodup.ext]

Deduplication Equality Criterion for Multisets

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the deduplication of $s$ equals the deduplication of $t$ if and only if every element $a$ belongs to $s$ exactly when it belongs to $t$. In other words, $\text{dedup}(s) = \text{dedup}(t) \leftrightarrow (\forall a, a \in s \leftrightarrow a \in t)$.

Multiset.dedup_map_of_injective theorem

[DecidableEq β] {f : α → β} (hf : Function.Injective f) (s : Multiset α) : (s.map f).dedup = s.dedup.map f

Full source

theorem dedup_map_of_injective [DecidableEq β] {f : α → β} (hf : Function.Injective f)
    (s : Multiset α) :
    (s.map f).dedup = s.dedup.map f :=
  Quot.induction_on s fun l => by simp [List.dedup_map_of_injective hf l]

Deduplication Commutes with Injective Mapping of Multisets

Informal description

Let $f : \alpha \to \beta$ be an injective function and $s$ be a multiset over $\alpha$. Then the deduplication of the image of $s$ under $f$ is equal to the image of the deduplication of $s$ under $f$, i.e., \[ \text{dedup}(f(s)) = f(\text{dedup}(s)). \]

Multiset.dedup_map_dedup_eq theorem

[DecidableEq β] (f : α → β) (s : Multiset α) : dedup (map f (dedup s)) = dedup (map f s)

Full source

theorem dedup_map_dedup_eq [DecidableEq β] (f : α → β) (s : Multiset α) :
    dedup (map f (dedup s)) = dedup (map f s) := by
  simp [dedup_ext]

Deduplication Commutes with Mapping: $\text{dedup} \circ \text{map}\, f \circ \text{dedup} = \text{dedup} \circ \text{map}\, f$

Informal description

For any function $f : \alpha \to \beta$ and multiset $s$ over $\alpha$, the deduplication of the image of $f$ applied to the deduplicated $s$ is equal to the deduplication of the image of $f$ applied to $s$. That is, $\text{dedup}(\text{map}\, f (\text{dedup}\, s)) = \text{dedup}(\text{map}\, f\, s)$.

Multiset.Nodup.le_dedup_iff_le theorem

{s t : Multiset α} (hno : s.Nodup) : s ≤ t.dedup ↔ s ≤ t

Full source

theorem Nodup.le_dedup_iff_le {s t : Multiset α} (hno : s.Nodup) : s ≤ t.dedup ↔ s ≤ t := by
  simp [le_dedup, hno]

Submultiset Relation Preserved Under Deduplication for Nodup Multisets

Informal description

For any multisets $s$ and $t$ of type $\alpha$, if $s$ has no duplicates ($s.\text{Nodup}$), then $s$ is a submultiset of the deduplicated version of $t$ if and only if $s$ is a submultiset of $t$. In other words, $s \leq t.\text{dedup} \leftrightarrow s \leq t$.

Multiset.Subset.dedup_add_right theorem

{s t : Multiset α} (h : s ⊆ t) : dedup (s + t) = dedup t

Full source

theorem Subset.dedup_add_right {s t : Multiset α} (h : s ⊆ t) :
    dedup (s + t) = dedup t := by
  induction s, t using Quot.induction_on₂
  exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.dedup_append_right h

Deduplication of Sum with Submultiset: $\text{dedup}(s + t) = \text{dedup}(t)$ when $s \subseteq t$

Informal description

For any multisets $s$ and $t$ of type $\alpha$, if $s$ is a submultiset of $t$ (i.e., $s \subseteq t$), then the deduplication of the sum $s + t$ is equal to the deduplication of $t$, i.e., $\text{dedup}(s + t) = \text{dedup}(t)$.

Multiset.Subset.dedup_add_left theorem

{s t : Multiset α} (h : t ⊆ s) : dedup (s + t) = dedup s

Full source

theorem Subset.dedup_add_left {s t : Multiset α} (h : t ⊆ s) :
    dedup (s + t) = dedup s := by
  rw [s.add_comm, Subset.dedup_add_right h]

Deduplication of Sum with Submultiset: $\text{dedup}(s + t) = \text{dedup}(s)$ when $t \subseteq s$

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, if $t$ is a submultiset of $s$ (i.e., $t \subseteq s$), then the deduplication of the sum $s + t$ is equal to the deduplication of $s$, i.e., $\text{dedup}(s + t) = \text{dedup}(s)$.

Multiset.Disjoint.dedup_add theorem

{s t : Multiset α} (h : Disjoint s t) : dedup (s + t) = dedup s + dedup t

Full source

theorem Disjoint.dedup_add {s t : Multiset α} (h : Disjoint s t) :
    dedup (s + t) = dedup s + dedup t := by
  induction s, t using Quot.induction_on₂
  exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.dedup_append (by simpa using h)

Deduplication Preserves Addition for Disjoint Multisets

Informal description

For any two disjoint multisets $s$ and $t$ over a type $\alpha$, the deduplication of their sum equals the sum of their deduplications, i.e., $\text{dedup}(s + t) = \text{dedup}(s) + \text{dedup}(t)$.

List.Subset.dedup_append_left theorem

{s t : List α} (h : t ⊆ s) : List.dedup (s ++ t) ~ List.dedup s

Full source

/-- Note that the stronger `List.Subset.dedup_append_right` is proved earlier. -/
theorem _root_.List.Subset.dedup_append_left {s t : List α} (h : t ⊆ s) :
    List.dedupList.dedup (s ++ t) ~ List.dedup s := by
  rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]

Deduplication of Concatenation with Sublist: $\text{dedup}(s \mathbin{+\kern-1.5ex+} t) \sim \text{dedup}(s)$ when $t \subseteq s$

Informal description

For any two lists $s$ and $t$ of elements of type $\alpha$, if $t$ is a sublist of $s$ (i.e., every element of $t$ appears in $s$), then the deduplicated version of the concatenation $s \mathbin{+\kern-1.5ex+} t$ is equivalent (under list permutation) to the deduplicated version of $s$.