# 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`.

source
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.

- cons_mem {α : Type u_1} {x : α} {l : List α} : x ∈ l → Duplicate x (x :: l)
- cons_duplicate {α : Type u_1} {x y : α} {l : List α} : Duplicate x l → Duplicate x (y :: l)

Instances For

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

The contrapositive of `List.nodup_iff_sublist`.

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

- List.decidableDuplicate x [] = isFalse ⋯
- List.decidableDuplicate x (y :: l) = match List.decidableDuplicate x l with | isTrue h => isTrue ⋯ | isFalse h => if hx : y = x ∧ x ∈ l then isTrue ⋯ else isFalse ⋯