# Erasing duplicates in a multiset. #

### dedup #

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

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

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

Alias of the reverse direction of Multiset.dedup_eq_self.

theorem Multiset.count_dedup {α : Type u_1} [] (m : ) (a : α) :
Multiset.count a m.dedup = if a m then 1 else 0
@[simp]
theorem Multiset.dedup_idem {α : Type u_1} [] {m : } :
m.dedup.dedup = m.dedup
theorem Multiset.dedup_eq_zero {α : Type u_1} [] {s : } :
s.dedup = 0 s = 0
@[simp]
theorem Multiset.dedup_singleton {α : Type u_1} [] {a : α} :
{a}.dedup = {a}
theorem Multiset.le_dedup {α : Type u_1} [] {s : } {t : } :
s t.dedup s t s.Nodup
theorem Multiset.le_dedup_self {α : Type u_1} [] {s : } :
s s.dedup s.Nodup
theorem Multiset.dedup_ext {α : Type u_1} [] {s : } {t : } :
s.dedup = t.dedup ∀ (a : α), a s a t
theorem Multiset.dedup_map_dedup_eq {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (s : ) :
(Multiset.map f s.dedup).dedup = ().dedup
@[simp]
theorem Multiset.dedup_nsmul {α : Type u_1} [] {s : } {n : } (h0 : n 0) :
(n s).dedup = s.dedup
theorem Multiset.Nodup.le_dedup_iff_le {α : Type u_1} [] {s : } {t : } (hno : s.Nodup) :
s t.dedup s t
theorem Multiset.Nodup.le_nsmul_iff_le {α : Type u_1} {s : } {t : } {n : } (h : s.Nodup) (hn : n 0) :
s n t s t