Documentation

Mathlib.Data.Multiset.Dedup

Erasing duplicates in a multiset. #

dedup #

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

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

Equations
Instances For
    @[simp]
    theorem Multiset.coe_dedup {α : Type u_1} [DecidableEq α] (l : List α) :
    (↑l).dedup = l.dedup
    @[simp]
    theorem Multiset.dedup_zero {α : Type u_1} [DecidableEq α] :
    @[simp]
    theorem Multiset.mem_dedup {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
    a s.dedup a s
    @[simp]
    theorem Multiset.dedup_cons_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
    a s(a ::ₘ s).dedup = s.dedup
    @[simp]
    theorem Multiset.dedup_cons_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
    as(a ::ₘ s).dedup = a ::ₘ s.dedup
    theorem Multiset.dedup_le {α : Type u_1} [DecidableEq α] (s : Multiset α) :
    s.dedup s
    theorem Multiset.dedup_subset {α : Type u_1} [DecidableEq α] (s : Multiset α) :
    s.dedup s
    theorem Multiset.subset_dedup {α : Type u_1} [DecidableEq α] (s : Multiset α) :
    s s.dedup
    @[simp]
    theorem Multiset.dedup_subset' {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
    s.dedup t s t
    @[simp]
    theorem Multiset.subset_dedup' {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
    s t.dedup s t
    @[simp]
    theorem Multiset.nodup_dedup {α : Type u_1} [DecidableEq α] (s : Multiset α) :
    s.dedup.Nodup
    theorem Multiset.dedup_eq_self {α : Type u_1} [DecidableEq α] {s : Multiset α} :
    s.dedup = s s.Nodup
    theorem Multiset.Nodup.dedup {α : Type u_1} [DecidableEq α] {s : Multiset α} :
    s.Nodups.dedup = s

    Alias of the reverse direction of Multiset.dedup_eq_self.

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

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

    theorem Multiset.Nodup.le_nsmul_iff_le {α : Type u_1} {s : Multiset α} {t : Multiset α} {n : } (h : s.Nodup) (hn : n 0) :
    s n t s t