Documentation

Mathlib.Data.Multiset.Dedup

Erasing duplicates in a multiset. #

dedup #

source
def Multiset.dedup {α : Type u_1} [DecidableEq α] (s : Multiset α) :
Multiset α

dedup s removes duplicates from s, yielding a nodup multiset.

Equations
    Instances For
      source
      @[simp]
      theorem Multiset.coe_dedup {α : Type u_1} [DecidableEq α] (l : List α) :
      (↑l).dedup = ↑l.dedup
      source
      @[simp]
      theorem Multiset.dedup_zero {α : Type u_1} [DecidableEq α] :
      dedup 0 = 0
      source
      @[simp]
      theorem Multiset.mem_dedup {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
      a ∈ s.dedup ↔ a ∈ s
      source
      @[simp]
      theorem Multiset.dedup_cons_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
      a ∈ s → (a ::ₘ s).dedup = s.dedup
      source
      @[simp]
      theorem Multiset.dedup_cons_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
      a ∉ s → (a ::ₘ s).dedup = a ::ₘ s.dedup
      source
      @[deprecated Multiset.dedup_cons_of_notMem (since := "2025-05-23")]
      theorem Multiset.dedup_cons_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
      a ∉ s → (a ::ₘ s).dedup = a ::ₘ s.dedup

      Alias of Multiset.dedup_cons_of_notMem.

      source
      theorem Multiset.dedup_le {α : Type u_1} [DecidableEq α] (s : Multiset α) :
      s.dedup ≤ s
      source
      theorem Multiset.dedup_subset {α : Type u_1} [DecidableEq α] (s : Multiset α) :
      s.dedup ⊆ s
      source
      theorem Multiset.subset_dedup {α : Type u_1} [DecidableEq α] (s : Multiset α) :
      s ⊆ s.dedup
      source
      @[simp]
      theorem Multiset.dedup_subset' {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
      s.dedup ⊆ t ↔ s ⊆ t
      source
      @[simp]
      theorem Multiset.subset_dedup' {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
      s ⊆ t.dedup ↔ s ⊆ t
      source
      @[simp]
      theorem Multiset.nodup_dedup {α : Type u_1} [DecidableEq α] (s : Multiset α) :
      s.dedup.Nodup
      source
      theorem Multiset.dedup_eq_self {α : Type u_1} [DecidableEq α] {s : Multiset α} :
      s.dedup = s ↔ s.Nodup
      source
      theorem Multiset.Nodup.dedup {α : Type u_1} [DecidableEq α] {s : Multiset α} :
      s.Nodup → s.dedup = s

      Alias of the reverse direction of Multiset.dedup_eq_self.

      source
      theorem Multiset.count_dedup {α : Type u_1} [DecidableEq α] (m : Multiset α) (a : α) :
      count a m.dedup = if a ∈ m then 1 else 0
      source
      @[simp]
      theorem Multiset.dedup_idem {α : Type u_1} [DecidableEq α] {m : Multiset α} :
      m.dedup.dedup = m.dedup
      source
      theorem Multiset.dedup_eq_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} :
      s.dedup = 0 ↔ s = 0
      source
      @[simp]
      theorem Multiset.dedup_singleton {α : Type u_1} [DecidableEq α] {a : α} :
      {a}.dedup = {a}
      source
      theorem Multiset.le_dedup {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
      s ≤ t.dedup ↔ s ≤ t ∧ s.Nodup
      source
      theorem Multiset.le_dedup_self {α : Type u_1} [DecidableEq α] {s : Multiset α} :
      s ≤ s.dedup ↔ s.Nodup
      source
      theorem Multiset.dedup_ext {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
      s.dedup = t.dedup ↔ ∀ (a : α), a ∈ s ↔ a ∈ t
      source
      theorem Multiset.dedup_map_of_injective {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (s : Multiset α) :
      (map f s).dedup = map f s.dedup
      source
      theorem Multiset.dedup_map_dedup_eq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) :
      (map f s.dedup).dedup = (map f s).dedup
      source
      theorem Multiset.Nodup.le_dedup_iff_le {α : Type u_1} [DecidableEq α] {s t : Multiset α} (hno : s.Nodup) :
      s ≤ t.dedup ↔ s ≤ t
      source
      theorem Multiset.Subset.dedup_add_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ⊆ t) :
      (s + t).dedup = t.dedup
      source
      theorem Multiset.Subset.dedup_add_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : t ⊆ s) :
      (s + t).dedup = s.dedup
      source
      theorem Multiset.Disjoint.dedup_add {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : Disjoint s t) :
      (s + t).dedup = s.dedup + t.dedup
      source
      theorem List.Subset.dedup_append_left {α : Type u_1} [DecidableEq α] {s t : List α} (h : t ⊆ s) :
      (s ++ t).dedup.Perm s.dedup

      Note that the stronger List.Subset.dedup_append_right is proved earlier.