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
theorem
List.dedup_cons_of_mem'
{α : Type u}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : a ∈ List.dedup l)
:
List.dedup (a :: l) = List.dedup l
theorem
List.dedup_cons_of_not_mem'
{α : Type u}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : ¬a ∈ List.dedup l)
:
List.dedup (a :: l) = a :: List.dedup l
@[simp]
theorem
List.mem_dedup
{α : Type u}
[inst : DecidableEq α]
{a : α}
{l : List α}
:
a ∈ List.dedup l ↔ a ∈ l
@[simp]
theorem
List.dedup_cons_of_mem
{α : Type u}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : a ∈ l)
:
List.dedup (a :: l) = List.dedup l
@[simp]
theorem
List.dedup_cons_of_not_mem
{α : Type u}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : ¬a ∈ l)
:
List.dedup (a :: l) = a :: List.dedup l
theorem
List.dedup_sublist
{α : Type u}
[inst : DecidableEq α]
(l : List α)
:
List.Sublist (List.dedup l) l
theorem
List.nodup_dedup
{α : Type u}
[inst : DecidableEq α]
(l : List α)
:
List.Nodup (List.dedup l)
theorem
List.dedup_eq_self
{α : Type u}
[inst : DecidableEq α]
{l : List α}
:
List.dedup l = l ↔ List.Nodup l
theorem
List.Nodup.dedup
{α : Type u}
[inst : DecidableEq α]
{l : List α}
(h : List.Nodup l)
:
List.dedup l = l
@[simp]
theorem
List.dedup_idempotent
{α : Type u}
[inst : DecidableEq α]
{l : List α}
:
List.dedup (List.dedup l) = List.dedup l
theorem
List.dedup_append
{α : Type u}
[inst : DecidableEq α]
(l₁ : List α)
(l₂ : List α)
:
List.dedup (l₁ ++ l₂) = l₁ ∪ List.dedup l₂
theorem
List.replicate_dedup
{α : Type u}
[inst : DecidableEq α]
{x : α}
{k : ℕ}
:
k ≠ 0 → List.dedup (List.replicate k x) = [x]
theorem
List.count_dedup
{α : Type u}
[inst : DecidableEq α]
(l : List α)
(a : α)
:
List.count a (List.dedup l) = if a ∈ l then 1 else 0
theorem
List.sum_map_count_dedup_filter_eq_countp
{α : Type u}
[inst : DecidableEq α]
(p : α → Bool)
(l : List α)
:
List.sum (List.map (fun x => List.count x l) (List.filter p (List.dedup l))) = List.countp p l
Summing the count of x over a list filtered by some p is just countp applied to p
theorem
List.sum_map_count_dedup_eq_length
{α : Type u}
[inst : DecidableEq α]
(l : List α)
:
List.sum (List.map (fun x => List.count x l) (List.dedup l)) = List.length l