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.

• cons_mem: ∀ {α : Type u_1} {x : α} {l : List α}, x ∈ l → List.Duplicate x (x :: l)
• cons_duplicate: ∀ {α : Type u_1} {x y : α} {l : List α}, List.Duplicate x l → List.Duplicate x (y :: l)

Instances For

• List.decidableDuplicate

theorem List.Mem.duplicate_cons_self {α : Type u_1} {l : List α} {x : α} (h : x ∈ l) : List.Duplicate x (x :: l)

theorem List.Duplicate.duplicate_cons {α : Type u_1} {l : List α} {x : α} (h : List.Duplicate x l) (y : α) : List.Duplicate x (y :: l)

theorem List.Duplicate.mem {α : Type u_1} {l : List α} {x : α} (h : List.Duplicate x l) : 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 : List.Duplicate x l) : l ≠ []

@[simp]

theorem List.not_duplicate_nil {α : Type u_1} (x : α) : ¬List.Duplicate x []

theorem List.Duplicate.ne_singleton {α : Type u_1} {l : List α} {x : α} (h : List.Duplicate x l) (y : α) : l ≠ [y]

@[simp]

theorem List.not_duplicate_singleton {α : Type u_1} (x y : α) : ¬List.Duplicate x [y]

theorem List.Duplicate.elim_nil {α : Type u_1} {x : α} (h : List.Duplicate x []) : False

theorem List.Duplicate.elim_singleton {α : Type u_1} {x y : α} (h : List.Duplicate x [y]) : False

theorem List.duplicate_cons_iff {α : Type u_1} {l : List α} {x y : α} : List.Duplicate x (y :: l) ↔ y = x ∧ x ∈ l ∨ List.Duplicate x l

theorem List.Duplicate.of_duplicate_cons {α : Type u_1} {l : List α} {x y : α} (h : List.Duplicate x (y :: l)) (hx : x ≠ y) : List.Duplicate x l

theorem List.duplicate_cons_iff_of_ne {α : Type u_1} {l : List α} {x y : α} (hne : x ≠ y) : List.Duplicate x (y :: l) ↔ List.Duplicate x l

theorem List.Duplicate.mono_sublist {α : Type u_1} {l : List α} {x : α} {l' : List α} (hx : List.Duplicate x l) (h : l.Sublist l') : List.Duplicate x l'

theorem List.duplicate_iff_sublist {α : Type u_1} {l : List α} {x : α} : List.Duplicate x l ↔ [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 : α), ¬List.Duplicate x l

theorem List.exists_duplicate_iff_not_nodup {α : Type u_1} {l : List α} : (∃ (x : α), List.Duplicate x l) ↔ ¬l.Nodup

theorem List.Duplicate.not_nodup {α : Type u_1} {l : List α} {x : α} (h : List.Duplicate x l) : ¬l.Nodup

theorem List.duplicate_iff_two_le_count {α : Type u_1} {l : List α} {x : α} [DecidableEq α] : List.Duplicate x l ↔ 2 ≤ List.count x l

instance List.decidableDuplicate {α : Type u_1} [DecidableEq α] (x : α) (l : List α) : Decidable (List.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 ⋯