mathlib3 documentation

data.multiset.dedup

Erasing duplicates in a multiset. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

dedup #

def multiset.dedup {α : Type u_1} [decidable_eq α] (s : multiset α) :

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

Equations
@[simp]
theorem multiset.coe_dedup {α : Type u_1} [decidable_eq α] (l : list α) :
@[simp]
theorem multiset.dedup_zero {α : Type u_1} [decidable_eq α] :
0.dedup = 0
@[simp]
theorem multiset.mem_dedup {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a s.dedup a s
@[simp]
theorem multiset.dedup_cons_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a s (a ::ₘ s).dedup = s.dedup
@[simp]
theorem multiset.dedup_cons_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a s (a ::ₘ s).dedup = a ::ₘ s.dedup
theorem multiset.dedup_le {α : Type u_1} [decidable_eq α] (s : multiset α) :
theorem multiset.dedup_subset {α : Type u_1} [decidable_eq α] (s : multiset α) :
theorem multiset.subset_dedup {α : Type u_1} [decidable_eq α] (s : multiset α) :
@[simp]
theorem multiset.dedup_subset' {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s.dedup t s t
@[simp]
theorem multiset.subset_dedup' {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s t.dedup s t
@[simp]
theorem multiset.nodup_dedup {α : Type u_1} [decidable_eq α] (s : multiset α) :
theorem multiset.dedup_eq_self {α : Type u_1} [decidable_eq α] {s : multiset α} :
theorem multiset.nodup.dedup {α : Type u_1} [decidable_eq α] {s : multiset α} :

Alias of the reverse direction of multiset.dedup_eq_self.

theorem multiset.count_dedup {α : Type u_1} [decidable_eq α] (m : multiset α) (a : α) :
multiset.count a m.dedup = ite (a m) 1 0
@[simp]
theorem multiset.dedup_idempotent {α : Type u_1} [decidable_eq α] {m : multiset α} :
@[simp]
theorem multiset.dedup_bind_dedup {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (m : multiset α) (f : α multiset β) :
(m.dedup.bind f).dedup = (m.bind f).dedup
theorem multiset.dedup_eq_zero {α : Type u_1} [decidable_eq α] {s : multiset α} :
s.dedup = 0 s = 0
@[simp]
theorem multiset.dedup_singleton {α : Type u_1} [decidable_eq α] {a : α} :
{a}.dedup = {a}
theorem multiset.le_dedup {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s t.dedup s t s.nodup
theorem multiset.le_dedup_self {α : Type u_1} [decidable_eq α] {s : multiset α} :
theorem multiset.dedup_ext {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s.dedup = t.dedup (a : α), a s a t
theorem multiset.dedup_map_dedup_eq {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α β) (s : multiset α) :
@[simp]
theorem multiset.dedup_nsmul {α : Type u_1} [decidable_eq α] {s : multiset α} {n : } (h0 : n 0) :
(n s).dedup = s.dedup
theorem multiset.nodup.le_dedup_iff_le {α : Type u_1} [decidable_eq α] {s t : multiset α} (hno : s.nodup) :
s t.dedup s t
theorem multiset.nodup.le_nsmul_iff_le {α : Type u_1} {s t : multiset α} {n : } (h : s.nodup) (hn : n 0) :
s n t s t