mathlib documentation

data.multiset.erase_dup

Erasing duplicates in a multiset.

erase_dup

def multiset.erase_dup {α : Type u_1} [decidable_eq α] :
multiset αmultiset α

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

Equations
@[simp]
theorem multiset.coe_erase_dup {α : Type u_1} [decidable_eq α] (l : list α) :

@[simp]
theorem multiset.erase_dup_zero {α : Type u_1} [decidable_eq α] :

@[simp]
theorem multiset.mem_erase_dup {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :

@[simp]
theorem multiset.erase_dup_cons_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a s(a ::ₘ s).erase_dup = s.erase_dup

@[simp]
theorem multiset.erase_dup_cons_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a s(a ::ₘ s).erase_dup = a ::ₘ s.erase_dup

theorem multiset.erase_dup_le {α : Type u_1} [decidable_eq α] (s : multiset α) :

theorem multiset.erase_dup_subset {α : Type u_1} [decidable_eq α] (s : multiset α) :

theorem multiset.subset_erase_dup {α : Type u_1} [decidable_eq α] (s : multiset α) :

@[simp]
theorem multiset.erase_dup_subset' {α : Type u_1} [decidable_eq α] {s t : multiset α} :

@[simp]
theorem multiset.subset_erase_dup' {α : Type u_1} [decidable_eq α] {s t : multiset α} :

@[simp]
theorem multiset.nodup_erase_dup {α : Type u_1} [decidable_eq α] (s : multiset α) :

theorem multiset.erase_dup_eq_self {α : Type u_1} [decidable_eq α] {s : multiset α} :

theorem multiset.erase_dup_eq_zero {α : Type u_1} [decidable_eq α] {s : multiset α} :
s.erase_dup = 0 s = 0

@[simp]
theorem multiset.erase_dup_singleton {α : Type u_1} [decidable_eq α] {a : α} :

theorem multiset.le_erase_dup {α : Type u_1} [decidable_eq α] {s t : multiset α} :

theorem multiset.erase_dup_ext {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s.erase_dup = t.erase_dup ∀ (a : α), a s a t

theorem multiset.erase_dup_map_erase_dup_eq {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α → β) (s : multiset α) :