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

@[simp]
theorem List.dedup_nil {α : Type u_1} [DecidableEq α] :
[].dedup = []
theorem List.dedup_cons_of_mem' {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a l.dedup) :
(a :: l).dedup = l.dedup
theorem List.dedup_cons_of_not_mem' {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : al.dedup) :
(a :: l).dedup = a :: l.dedup
@[simp]
theorem List.mem_dedup {α : Type u_1} [DecidableEq α] {a : α} {l : List α} :
a l.dedup a l
@[simp]
theorem List.dedup_cons_of_mem {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a l) :
(a :: l).dedup = l.dedup
@[simp]
theorem List.dedup_cons_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : al) :
(a :: l).dedup = a :: l.dedup
theorem List.dedup_sublist {α : Type u_1} [DecidableEq α] (l : List α) :
l.dedup.Sublist l
theorem List.dedup_subset {α : Type u_1} [DecidableEq α] (l : List α) :
l.dedup l
theorem List.subset_dedup {α : Type u_1} [DecidableEq α] (l : List α) :
l l.dedup
theorem List.nodup_dedup {α : Type u_1} [DecidableEq α] (l : List α) :
l.dedup.Nodup
theorem List.headI_dedup {α : Type u_1} [DecidableEq α] [Inhabited α] (l : List α) :
l.dedup.headI = if l.headI l.tail then l.tail.dedup.headI else l.headI
theorem List.tail_dedup {α : Type u_1} [DecidableEq α] [Inhabited α] (l : List α) :
l.dedup.tail = if l.headI l.tail then l.tail.dedup.tail else l.tail.dedup
theorem List.dedup_eq_self {α : Type u_1} [DecidableEq α] {l : List α} :
l.dedup = l l.Nodup
theorem List.dedup_eq_cons {α : Type u_1} [DecidableEq α] (l : List α) (a : α) (l' : List α) :
l.dedup = a :: l' a l al' l.dedup.tail = l'
@[simp]
theorem List.dedup_eq_nil {α : Type u_1} [DecidableEq α] (l : List α) :
l.dedup = [] l = []
theorem List.Nodup.dedup {α : Type u_1} [DecidableEq α] {l : List α} (h : l.Nodup) :
l.dedup = l
@[simp]
theorem List.dedup_idem {α : Type u_1} [DecidableEq α] {l : List α} :
l.dedup.dedup = l.dedup
theorem List.dedup_append {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
(l₁ ++ l₂).dedup = l₁ l₂.dedup
theorem List.dedup_map_of_injective {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : αβ} (hf : Function.Injective f) (xs : List α) :
(List.map f xs).dedup = List.map f xs.dedup
theorem List.Subset.dedup_append_right {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List α} (h : xs ys) :
(xs ++ ys).dedup = ys.dedup

Note that the weaker List.Subset.dedup_append_left is proved later.

theorem List.Disjoint.union_eq {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List α} (h : xs.Disjoint ys) :
xs ys = xs.dedup ++ ys
theorem List.Disjoint.dedup_append {α : Type u_1} [DecidableEq α] {xs : List α} {ys : List α} (h : xs.Disjoint ys) :
(xs ++ ys).dedup = xs.dedup ++ ys.dedup
theorem List.replicate_dedup {α : Type u_1} [DecidableEq α] {x : α} {k : } :
k 0(List.replicate k x).dedup = [x]
theorem List.count_dedup {α : Type u_1} [DecidableEq α] (l : List α) (a : α) :
List.count a l.dedup = if a l then 1 else 0