mathlib documentation

data.list.nodup

Lists with no duplicates

list.nodup is defined in data/list/defs. In this file we prove various properties of this predicate.

@[simp]
theorem list.forall_mem_ne {α : Type u} {a : α} {l : list α} :
(∀ (a' : α), a' l¬a = a') a l

@[simp]
theorem list.nodup_nil {α : Type u} :

@[simp]
theorem list.nodup_cons {α : Type u} {a : α} {l : list α} :
(a :: l).nodup a l l.nodup

theorem list.rel_nodup {α : Type u} {β : Type v} {r : α → β → Prop} :

theorem list.nodup_cons_of_nodup {α : Type u} {a : α} {l : list α} :
a ll.nodup(a :: l).nodup

theorem list.nodup_singleton {α : Type u} (a : α) :
[a].nodup

theorem list.nodup_of_nodup_cons {α : Type u} {a : α} {l : list α} :
(a :: l).nodup → l.nodup

theorem list.not_mem_of_nodup_cons {α : Type u} {a : α} {l : list α} :
(a :: l).nodupa l

theorem list.not_nodup_cons_of_mem {α : Type u} {a : α} {l : list α} :
a l¬(a :: l).nodup

theorem list.nodup_of_sublist {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂l₂.nodup → l₁.nodup

theorem list.not_nodup_pair {α : Type u} (a : α) :
¬[a, a].nodup

theorem list.nodup_iff_sublist {α : Type u} {l : list α} :
l.nodup ∀ (a : α), ¬[a, a] <+ l

theorem list.nodup_iff_nth_le_inj {α : Type u} {l : list α} :
l.nodup ∀ (i j : ) (h₁ : i < l.length) (h₂ : j < l.length), l.nth_le i h₁ = l.nth_le j h₂i = j

@[simp]
theorem list.nth_le_index_of {α : Type u} [decidable_eq α] {l : list α} (H : l.nodup) (n : ) (h : n < l.length) :
list.index_of (l.nth_le n h) l = n

theorem list.nodup_iff_count_le_one {α : Type u} [decidable_eq α] {l : list α} :
l.nodup ∀ (a : α), list.count a l 1

theorem list.nodup_repeat {α : Type u} (a : α) {n : } :

@[simp]
theorem list.count_eq_one_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} :
l.nodupa llist.count a l = 1

theorem list.nodup_of_nodup_append_left {α : Type u} {l₁ l₂ : list α} :
(l₁ ++ l₂).nodup → l₁.nodup

theorem list.nodup_of_nodup_append_right {α : Type u} {l₁ l₂ : list α} :
(l₁ ++ l₂).nodup → l₂.nodup

theorem list.nodup_append {α : Type u} {l₁ l₂ : list α} :
(l₁ ++ l₂).nodup l₁.nodup l₂.nodup l₁.disjoint l₂

theorem list.disjoint_of_nodup_append {α : Type u} {l₁ l₂ : list α} :
(l₁ ++ l₂).nodupl₁.disjoint l₂

theorem list.nodup_append_of_nodup {α : Type u} {l₁ l₂ : list α} :
l₁.nodupl₂.nodupl₁.disjoint l₂(l₁ ++ l₂).nodup

theorem list.nodup_append_comm {α : Type u} {l₁ l₂ : list α} :
(l₁ ++ l₂).nodup (l₂ ++ l₁).nodup

theorem list.nodup_middle {α : Type u} {a : α} {l₁ l₂ : list α} :
(l₁ ++ a :: l₂).nodup (a :: (l₁ ++ l₂)).nodup

theorem list.nodup_of_nodup_map {α : Type u} {β : Type v} (f : α → β) {l : list α} :
(list.map f l).nodup → l.nodup

theorem list.nodup_map_on {α : Type u} {β : Type v} {f : α → β} {l : list α} :
(∀ (x : α), x l∀ (y : α), y lf x = f yx = y)l.nodup(list.map f l).nodup

theorem list.nodup_map {α : Type u} {β : Type v} {f : α → β} {l : list α} :

theorem list.nodup_map_iff {α : Type u} {β : Type v} {f : α → β} {l : list α} :

@[simp]
theorem list.nodup_attach {α : Type u} {l : list α} :

theorem list.nodup_pmap {α : Type u} {β : Type v} {p : α → Prop} {f : Π (a : α), p a → β} {l : list α} {H : ∀ (a : α), a lp a} :
(∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hba = b)l.nodup(list.pmap f l H).nodup

theorem list.nodup_filter {α : Type u} (p : α → Prop) [decidable_pred p] {l : list α} :
l.nodup(list.filter p l).nodup

@[simp]
theorem list.nodup_reverse {α : Type u} {l : list α} :

theorem list.nodup_erase_eq_filter {α : Type u} [decidable_eq α] (a : α) {l : list α} :
l.nodupl.erase a = list.filter (λ (_x : α), _x a) l

theorem list.nodup_erase_of_nodup {α : Type u} [decidable_eq α] (a : α) {l : list α} :
l.nodup(l.erase a).nodup

theorem list.nodup_diff {α : Type u} [decidable_eq α] {l₁ l₂ : list α} :
l₁.nodup(l₁.diff l₂).nodup

theorem list.mem_erase_iff_of_nodup {α : Type u} [decidable_eq α] {a b : α} {l : list α} :
l.nodup(a l.erase b a b a l)

theorem list.mem_erase_of_nodup {α : Type u} [decidable_eq α] {a : α} {l : list α} :
l.nodupa l.erase a

theorem list.nodup_join {α : Type u} {L : list (list α)} :
L.join.nodup (∀ (l : list α), l L → l.nodup) list.pairwise list.disjoint L

theorem list.nodup_bind {α : Type u} {β : Type v} {l₁ : list α} {f : α → list β} :
(l₁.bind f).nodup (∀ (x : α), x l₁(f x).nodup) list.pairwise (λ (a b : α), (f a).disjoint (f b)) l₁

theorem list.nodup_product {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} :
l₁.nodupl₂.nodup(l₁.product l₂).nodup

theorem list.nodup_sigma {α : Type u} {σ : α → Type u_1} {l₁ : list α} {l₂ : Π (a : α), list (σ a)} :
l₁.nodup(∀ (a : α), (l₂ a).nodup)(l₁.sigma l₂).nodup

theorem list.nodup_filter_map {α : Type u} {β : Type v} {f : α → option β} {l : list α} :
(∀ (a a' : α) (b : β), b f ab f a'a = a')l.nodup(list.filter_map f l).nodup

theorem list.nodup_concat {α : Type u} {a : α} {l : list α} :
a ll.nodup(l.concat a).nodup

theorem list.nodup_insert {α : Type u} [decidable_eq α] {a : α} {l : list α} :
l.nodup(insert a l).nodup

theorem list.nodup_union {α : Type u} [decidable_eq α] (l₁ : list α) {l₂ : list α} :
l₂.nodup(l₁ l₂).nodup

theorem list.nodup_inter_of_nodup {α : Type u} [decidable_eq α] {l₁ : list α} (l₂ : list α) :
l₁.nodup(l₁ l₂).nodup

@[simp]
theorem list.nodup_sublists {α : Type u} {l : list α} :

@[simp]
theorem list.nodup_sublists' {α : Type u} {l : list α} :

theorem list.nodup_sublists_len {α : Type u_1} (n : ) {l : list α} :

theorem list.diff_eq_filter_of_nodup {α : Type u} [decidable_eq α] {l₁ l₂ : list α} :
l₁.nodupl₁.diff l₂ = list.filter (λ (_x : α), _x l₂) l₁

theorem list.mem_diff_iff_of_nodup {α : Type u} [decidable_eq α] {l₁ l₂ : list α} (hl₁ : l₁.nodup) {a : α} :
a l₁.diff l₂ a l₁ a l₂

theorem list.nodup_update_nth {α : Type u} {l : list α} {n : } {a : α} :
l.nodupa l(l.update_nth n a).nodup

theorem list.nodup.map_update {α : Type u} {β : Type v} [decidable_eq α] {l : list α} (hl : l.nodup) (f : α → β) (x : α) (y : β) :
list.map (function.update f x y) l = ite (x l) ((list.map f l).update_nth (list.index_of x l) y) (list.map f l)

theorem option.to_list_nodup {α : Type u_1} (o : option α) :