# List duplicates #

## Main definitions #

• List.Duplicate x l : Prop is an inductive property that holds when x is a duplicate in l

## Implementation details #

In this file, x ∈+ l notation is shorthand for List.Duplicate x l.

inductive List.Duplicate {α : Type u_1} (x : α) :
List αProp

Property that an element x : α of l : List α can be found in the list more than once.

Instances For
theorem List.Mem.duplicate_cons_self {α : Type u_1} {l : List α} {x : α} (h : x l) :
theorem List.Duplicate.duplicate_cons {α : Type u_1} {l : List α} {x : α} (h : ) (y : α) :
theorem List.Duplicate.mem {α : Type u_1} {l : List α} {x : α} (h : ) :
x l
theorem List.Duplicate.mem_cons_self {α : Type u_1} {l : List α} {x : α} (h : List.Duplicate x (x :: l)) :
x l
@[simp]
theorem List.duplicate_cons_self_iff {α : Type u_1} {l : List α} {x : α} :
List.Duplicate x (x :: l) x l
theorem List.Duplicate.ne_nil {α : Type u_1} {l : List α} {x : α} (h : ) :
l []
@[simp]
theorem List.not_duplicate_nil {α : Type u_1} (x : α) :
theorem List.Duplicate.ne_singleton {α : Type u_1} {l : List α} {x : α} (h : ) (y : α) :
l [y]
@[simp]
theorem List.not_duplicate_singleton {α : Type u_1} (x : α) (y : α) :
theorem List.Duplicate.elim_nil {α : Type u_1} {x : α} (h : ) :
theorem List.Duplicate.elim_singleton {α : Type u_1} {x : α} {y : α} (h : List.Duplicate x [y]) :
theorem List.duplicate_cons_iff {α : Type u_1} {l : List α} {x : α} {y : α} :
List.Duplicate x (y :: l) y = x x l
theorem List.Duplicate.of_duplicate_cons {α : Type u_1} {l : List α} {x : α} {y : α} (h : List.Duplicate x (y :: l)) (hx : x y) :
theorem List.duplicate_cons_iff_of_ne {α : Type u_1} {l : List α} {x : α} {y : α} (hne : x y) :
theorem List.Duplicate.mono_sublist {α : Type u_1} {l : List α} {x : α} {l' : List α} (hx : ) (h : l.Sublist l') :
theorem List.duplicate_iff_sublist {α : Type u_1} {l : List α} {x : α} :
[x, x].Sublist l

The contrapositive of List.nodup_iff_sublist.

theorem List.nodup_iff_forall_not_duplicate {α : Type u_1} {l : List α} :
l.Nodup ∀ (x : α), ¬
theorem List.exists_duplicate_iff_not_nodup {α : Type u_1} {l : List α} :
(∃ (x : α), ) ¬l.Nodup
theorem List.Duplicate.not_nodup {α : Type u_1} {l : List α} {x : α} (h : ) :
¬l.Nodup
theorem List.duplicate_iff_two_le_count {α : Type u_1} {l : List α} {x : α} [] :
2
instance List.decidableDuplicate {α : Type u_1} [] (x : α) (l : List α) :
Equations