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

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)

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

source

theorem list.mem.duplicate_cons_self {α : Type u_1} {l : list α} {x : α} (h : x ∈ l) :

list.duplicate x (x :: l)

source

theorem list.duplicate.duplicate_cons {α : Type u_1} {l : list α} {x : α} (h : list.duplicate x l) (y : α) :

list.duplicate x (y :: l)

source

theorem list.duplicate.mem {α : Type u_1} {l : list α} {x : α} (h : list.duplicate x l) :

x ∈ l

source

theorem list.duplicate.mem_cons_self {α : Type u_1} {l : list α} {x : α} (h : list.duplicate x (x :: l)) :

x ∈ l

source

@[simp]

theorem list.duplicate_cons_self_iff {α : Type u_1} {l : list α} {x : α} :

list.duplicate x (x :: l) ↔ x ∈ l

source

theorem list.duplicate.ne_nil {α : Type u_1} {l : list α} {x : α} (h : list.duplicate x l) :

l ≠ list.nil

source

@[simp]

theorem list.not_duplicate_nil {α : Type u_1} (x : α) :

¬list.duplicate x list.nil

source

theorem list.duplicate.ne_singleton {α : Type u_1} {l : list α} {x : α} (h : list.duplicate x l) (y : α) :

l ≠ [y]

source

@[simp]

theorem list.not_duplicate_singleton {α : Type u_1} (x y : α) :

¬list.duplicate x [y]

source

theorem list.duplicate.elim_nil {α : Type u_1} {x : α} (h : list.duplicate x list.nil) :

false

source

theorem list.duplicate.elim_singleton {α : Type u_1} {x y : α} (h : list.duplicate x [y]) :

false

source

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

source

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

source

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

source

theorem list.duplicate.mono_sublist {α : Type u_1} {l : list α} {x : α} {l' : list α} (hx : list.duplicate x l) (h : l <+ l') :

list.duplicate x l'

source

theorem list.duplicate_iff_sublist {α : Type u_1} {l : list α} {x : α} :

list.duplicate x l ↔ [x, x] <+ l

The contrapositive of list.nodup_iff_sublist.

source

theorem list.nodup_iff_forall_not_duplicate {α : Type u_1} {l : list α} :

l.nodup ↔ ∀ (x : α), ¬list.duplicate x l

source

theorem list.exists_duplicate_iff_not_nodup {α : Type u_1} {l : list α} :

(∃ (x : α), list.duplicate x l) ↔ ¬l.nodup

source

theorem list.duplicate.not_nodup {α : Type u_1} {l : list α} {x : α} (h : list.duplicate x l) :

¬l.nodup

source

theorem list.duplicate_iff_two_le_count {α : Type u_1} {l : list α} {x : α} [decidable_eq α] :

list.duplicate x l ↔ 2 ≤ list.count x l

source

@[protected, instance]

def list.decidable_duplicate {α : Type u_1} [decidable_eq α] (x : α) (l : list α) :

decidable (list.duplicate x l)

Equations

list.decidable_duplicate x (y :: l) = list.decidable_duplicate._match_1 x y l (list.decidable_duplicate x l)
list.decidable_duplicate x list.nil = is_false _
list.decidable_duplicate._match_1 x y l (is_true h) = is_true _
list.decidable_duplicate._match_1 x y l (is_false h) = dite (y = x ∧ x ∈ l) (λ (hx : y = x ∧ x ∈ l), is_true _) (λ (hx : ¬(y = x ∧ x ∈ l)), is_false _)