mathlib3 documentation

data.list.dedup

Erasure of duplicates in a list #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [decidable_eq α] :
list.nil.dedup = list.nil
source
theorem list.dedup_cons_of_mem' {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a ∈ l.dedup) :
(a :: l).dedup = l.dedup
source
theorem list.dedup_cons_of_not_mem' {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a ∉ l.dedup) :
(a :: l).dedup = a :: l.dedup
source
@[simp]
theorem list.mem_dedup {α : Type u} [decidable_eq α] {a : α} {l : list α} :
a ∈ l.dedup ↔ a ∈ l
source
@[simp]
theorem list.dedup_cons_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a ∈ l) :
(a :: l).dedup = l.dedup
source
@[simp]
theorem list.dedup_cons_of_not_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a ∉ l) :
(a :: l).dedup = a :: l.dedup
source
theorem list.dedup_sublist {α : Type u} [decidable_eq α] (l : list α) :
l.dedup <+ l
source
theorem list.dedup_subset {α : Type u} [decidable_eq α] (l : list α) :
l.dedup ⊆ l
source
theorem list.subset_dedup {α : Type u} [decidable_eq α] (l : list α) :
l ⊆ l.dedup
source
theorem list.nodup_dedup {α : Type u} [decidable_eq α] (l : list α) :
l.dedup.nodup
source
theorem list.head_dedup {α : Type u} [decidable_eq α] [inhabited α] (l : list α) :
l.dedup.head = ite (l.head ∈ l.tail) l.tail.dedup.head l.head
source
theorem list.tail_dedup {α : Type u} [decidable_eq α] [inhabited α] (l : list α) :
l.dedup.tail = ite (l.head ∈ l.tail) l.tail.dedup.tail l.tail.dedup
source
theorem list.dedup_eq_self {α : Type u} [decidable_eq α] {l : list α} :
l.dedup = l ↔ l.nodup
source
theorem list.dedup_eq_cons {α : Type u} [decidable_eq α] (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} [decidable_eq α] (l : list α) :
l.dedup = list.nil ↔ l = list.nil
source
@[protected]
theorem list.nodup.dedup {α : Type u} [decidable_eq α] {l : list α} (h : l.nodup) :
l.dedup = l
source
@[simp]
theorem list.dedup_idempotent {α : Type u} [decidable_eq α] {l : list α} :
l.dedup.dedup = l.dedup
source
theorem list.dedup_append {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
(l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
source
theorem list.replicate_dedup {α : Type u} [decidable_eq α] {x : α} {k : ℕ} :
k ≠ 0 → (list.replicate k x).dedup = [x]
source
theorem list.count_dedup {α : Type u} [decidable_eq α] (l : list α) (a : α) :
list.count a l.dedup = ite (a ∈ l) 1 0
source
theorem list.sum_map_count_dedup_filter_eq_countp {α : Type u} [decidable_eq α] (p : α → Prop) [decidable_pred p] (l : list α) :
(list.map (λ (x : α), list.count x l) (list.filter p l.dedup)).sum = list.countp p l

Summing the count of x over a list filtered by some p is just countp applied to p

source
theorem list.sum_map_count_dedup_eq_length {α : Type u} [decidable_eq α] (l : list α) :
(list.map (λ (x : α), list.count x l) l.dedup).sum = l.length