Documentation

Mathlib.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

source
@[simp]
theorem List.dedup_nil {α : Type u} [DecidableEq α] :
[].dedup = []
source
theorem List.dedup_cons_of_mem' {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l.dedup) :
(a :: l).dedup = l.dedup
source
theorem List.dedup_cons_of_not_mem' {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∉ l.dedup) :
(a :: l).dedup = a :: l.dedup
source
@[simp]
theorem List.mem_dedup {α : Type u} [DecidableEq α] {a : α} {l : List α} :
a ∈ l.dedup ↔ a ∈ l
source
@[simp]
theorem List.dedup_cons_of_mem {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) :
(a :: l).dedup = l.dedup
source
@[simp]
theorem List.dedup_cons_of_not_mem {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∉ l) :
(a :: l).dedup = a :: l.dedup
source
theorem List.dedup_sublist {α : Type u} [DecidableEq α] (l : List α) :
l.dedup.Sublist l
source
theorem List.dedup_subset {α : Type u} [DecidableEq α] (l : List α) :
l.dedup ⊆ l
source
theorem List.subset_dedup {α : Type u} [DecidableEq α] (l : List α) :
l ⊆ l.dedup
source
theorem List.nodup_dedup {α : Type u} [DecidableEq α] (l : List α) :
l.dedup.Nodup
source
theorem List.headI_dedup {α : Type u} [DecidableEq α] [Inhabited α] (l : List α) :
l.dedup.headI = if l.headI ∈ l.tail then l.tail.dedup.headI else l.headI
source
theorem List.tail_dedup {α : Type u} [DecidableEq α] [Inhabited α] (l : List α) :
l.dedup.tail = if l.headI ∈ l.tail then l.tail.dedup.tail else l.tail.dedup
source
theorem List.dedup_eq_self {α : Type u} [DecidableEq α] {l : List α} :
l.dedup = l ↔ l.Nodup
source
theorem List.dedup_eq_cons {α : Type u} [DecidableEq α] (l : List α) (a : α) (l' : List α) :
l.dedup = a :: l' ↔ a ∈ l ∧ a ∉ l' ∧ l.dedup.tail = l'
source
@[simp]
theorem List.dedup_eq_nil {α : Type u} [DecidableEq α] (l : List α) :
l.dedup = [] ↔ l = []
source
theorem List.Nodup.dedup {α : Type u} [DecidableEq α] {l : List α} (h : l.Nodup) :
l.dedup = l
source
@[simp]
theorem List.dedup_idem {α : Type u} [DecidableEq α] {l : List α} :
l.dedup.dedup = l.dedup
source
theorem List.dedup_append {α : Type u} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
(l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
source
theorem List.replicate_dedup {α : Type u} [DecidableEq α] {x : α} {k : ℕ} :
k ≠ 0 → (List.replicate k x).dedup = [x]
source
theorem List.count_dedup {α : Type u} [DecidableEq α] (l : List α) (a : α) :
List.count a l.dedup = if a ∈ l then 1 else 0