mathlib documentation

data.list.dedup

Erasure of duplicates in a list #

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

Tags #

duplicate, multiplicity, nodup, nub

@[simp]
theorem list.dedup_nil {α : Type u} [decidable_eq α] :
theorem list.dedup_cons_of_mem' {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a l.dedup) :
(a :: l).dedup = l.dedup
theorem list.dedup_cons_of_not_mem' {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a l.dedup) :
(a :: l).dedup = a :: l.dedup
@[simp]
theorem list.mem_dedup {α : Type u} [decidable_eq α] {a : α} {l : list α} :
a l.dedup a l
@[simp]
theorem list.dedup_cons_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a l) :
(a :: l).dedup = l.dedup
@[simp]
theorem list.dedup_cons_of_not_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a l) :
(a :: l).dedup = a :: l.dedup
theorem list.dedup_sublist {α : Type u} [decidable_eq α] (l : list α) :
l.dedup <+ l
theorem list.dedup_subset {α : Type u} [decidable_eq α] (l : list α) :
theorem list.subset_dedup {α : Type u} [decidable_eq α] (l : list α) :
theorem list.nodup_dedup {α : Type u} [decidable_eq α] (l : list α) :
theorem list.dedup_eq_self {α : Type u} [decidable_eq α] {l : list α} :
@[protected]
theorem list.nodup.dedup {α : Type u} [decidable_eq α] {l : list α} (h : l.nodup) :
l.dedup = l
@[simp]
theorem list.dedup_idempotent {α : Type u} [decidable_eq α] {l : list α} :
theorem list.dedup_append {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
(l₁ ++ l₂).dedup = l₁ l₂.dedup
theorem list.repeat_dedup {α : Type u} [decidable_eq α] {x : α} {k : } :
k 0(list.repeat x k).dedup = [x]