mathlib documentation

data.list.erase_dup

@[simp]

theorem list.erase_dup_cons_of_mem' {α : Type u} [decidable_eq α] {a : α} {l : list α} :

theorem list.erase_dup_cons_of_not_mem' {α : Type u} [decidable_eq α] {a : α} {l : list α} :
a l.erase_dup(a :: l).erase_dup = a :: l.erase_dup

@[simp]
theorem list.mem_erase_dup {α : Type u} [decidable_eq α] {a : α} {l : list α} :

@[simp]
theorem list.erase_dup_cons_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} :
a l(a :: l).erase_dup = l.erase_dup

@[simp]
theorem list.erase_dup_cons_of_not_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} :
a l(a :: l).erase_dup = a :: l.erase_dup

theorem list.erase_dup_sublist {α : Type u} [decidable_eq α] (l : list α) :

theorem list.erase_dup_subset {α : Type u} [decidable_eq α] (l : list α) :

theorem list.subset_erase_dup {α : Type u} [decidable_eq α] (l : list α) :

theorem list.nodup_erase_dup {α : Type u} [decidable_eq α] (l : list α) :

theorem list.erase_dup_eq_self {α : Type u} [decidable_eq α] {l : list α} :

@[simp]
theorem list.erase_dup_idempotent {α : Type u} [decidable_eq α] {l : list α} :

theorem list.erase_dup_append {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
(l₁ ++ l₂).erase_dup = l₁ l₂.erase_dup