HepLean 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_1} [DecidableEq α] :
[].dedup = []
source
theorem List.dedup_cons_of_mem' {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l.dedup) :
(a :: l).dedup = l.dedup
source
theorem List.dedup_cons_of_not_mem' {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a ∉ l.dedup) :
(a :: l).dedup = a :: l.dedup
source
@[simp]
theorem List.mem_dedup {α : Type u_1} [DecidableEq α] {a : α} {l : List α} :
a ∈ l.dedup ↔ a ∈ l
source
@[simp]
theorem List.dedup_cons_of_mem {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) :
(a :: l).dedup = l.dedup
source
@[simp]
theorem List.dedup_cons_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a ∉ l) :
(a :: l).dedup = a :: l.dedup
source
theorem List.dedup_sublist {α : Type u_1} [DecidableEq α] (l : List α) :
l.dedup.Sublist l
source
theorem List.dedup_subset {α : Type u_1} [DecidableEq α] (l : List α) :
l.dedup ⊆ l
source
theorem List.subset_dedup {α : Type u_1} [DecidableEq α] (l : List α) :
l ⊆ l.dedup
source
theorem List.nodup_dedup {α : Type u_1} [DecidableEq α] (l : List α) :
l.dedup.Nodup
source
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
source
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
source
theorem List.dedup_eq_self {α : Type u_1} [DecidableEq α] {l : List α} :
l.dedup = l ↔ l.Nodup
source
theorem List.dedup_eq_cons {α : Type u_1} [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_1} [DecidableEq α] (l : List α) :
l.dedup = [] ↔ l = []
source
theorem List.Nodup.dedup {α : Type u_1} [DecidableEq α] {l : List α} (h : l.Nodup) :
l.dedup = l
source
@[simp]
theorem List.dedup_idem {α : Type u_1} [DecidableEq α] {l : List α} :
l.dedup.dedup = l.dedup
source
theorem List.dedup_append {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
(l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
source
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
source
theorem List.Subset.dedup_append_right {α : Type u_1} [DecidableEq α] {xs ys : List α} (h : xs ⊆ ys) :
(xs ++ ys).dedup = ys.dedup

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

source
theorem List.Disjoint.union_eq {α : Type u_1} [DecidableEq α] {xs ys : List α} (h : xs.Disjoint ys) :
xs ∪ ys = xs.dedup ++ ys
source
theorem List.Disjoint.dedup_append {α : Type u_1} [DecidableEq α] {xs ys : List α} (h : xs.Disjoint ys) :
(xs ++ ys).dedup = xs.dedup ++ ys.dedup
source
theorem List.replicate_dedup {α : Type u_1} [DecidableEq α] {x : α} {k : ℕ} :
k ≠ 0 → (List.replicate k x).dedup = [x]
source
theorem List.count_dedup {α : Type u_1} [DecidableEq α] (l : List α) (a : α) :
List.count a l.dedup = if a ∈ l then 1 else 0
source
theorem List.Perm.dedup {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} (p : l₁.Perm l₂) :
l₁.dedup.Perm l₂.dedup