mathlib documentation

data.list.erase_dup

Erasure of duplicates in a list #

This file proves basic results about list.erase_dup (definition in data.list.defs). erase_dup l returns l without its duplicates. It keeps the earliest (that is, rightmost) occurrence of each.

Tags #

duplicate, multiplicity, nodup, nub

source
@[simp]
theorem list.erase_dup_nil {α : Type u} [decidable_eq α] :
list.nil.erase_dup = list.nil
source
theorem list.erase_dup_cons_of_mem' {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a ∈ l.erase_dup) :
(a :: l).erase_dup = l.erase_dup
source
theorem list.erase_dup_cons_of_not_mem' {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a ∉ l.erase_dup) :
(a :: l).erase_dup = a :: l.erase_dup
source
@[simp]
theorem list.mem_erase_dup {α : Type u} [decidable_eq α] {a : α} {l : list α} :
a ∈ l.erase_dup ↔ a ∈ l
source
@[simp]
theorem list.erase_dup_cons_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a ∈ l) :
(a :: l).erase_dup = l.erase_dup
source
@[simp]
theorem list.erase_dup_cons_of_not_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a ∉ l) :
(a :: l).erase_dup = a :: l.erase_dup
source
theorem list.erase_dup_sublist {α : Type u} [decidable_eq α] (l : list α) :
l.erase_dup <+ l
source
theorem list.erase_dup_subset {α : Type u} [decidable_eq α] (l : list α) :
l.erase_dup ⊆ l
source
theorem list.subset_erase_dup {α : Type u} [decidable_eq α] (l : list α) :
l ⊆ l.erase_dup
source
theorem list.nodup_erase_dup {α : Type u} [decidable_eq α] (l : list α) :
l.erase_dup.nodup
source
theorem list.erase_dup_eq_self {α : Type u} [decidable_eq α] {l : list α} :
l.erase_dup = l ↔ l.nodup
source
@[protected]
theorem list.nodup.erase_dup {α : Type u} [decidable_eq α] {l : list α} (h : l.nodup) :
l.erase_dup = l
source
@[simp]
theorem list.erase_dup_idempotent {α : Type u} [decidable_eq α] {l : list α} :
l.erase_dup.erase_dup = l.erase_dup
source
theorem list.erase_dup_append {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
(l₁ ++ l₂).erase_dup = l₁ ∪ l₂.erase_dup