Lists with no duplicates

List.Nodup is defined in Data/List/Basic. In this file we prove various properties of this predicate.

theorem List.Pairwise.nodup {α : Type u} {l : List α} {r : α → α → Prop} [Std.Irrefl r] (h : Pairwise r l) : l.Nodup

theorem List.rel_nodup {α : Type u} {β : Type v} {r : α → β → Prop} (hr : Relator.BiUnique r) : Relator.LiftFun (Forall₂ r) (fun (x1 x2 : Prop) => x1 ↔ x2) Nodup Nodup

theorem List.Nodup.cons {α : Type u} {l : List α} {a : α} (ha : ¬a ∈ l) (hl : l.Nodup) : (a :: l).Nodup

theorem List.nodup_singleton {α : Type u} (a : α) : [a].Nodup

theorem List.Nodup.of_cons {α : Type u} {l : List α} {a : α} (h : (a :: l).Nodup) : l.Nodup

theorem List.Nodup.notMem {α : Type u} {l : List α} {a : α} (h : (a :: l).Nodup) : ¬a ∈ l

theorem List.not_nodup_cons_of_mem {α : Type u} {l : List α} {a : α} : a ∈ l → ¬(a :: 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].Sublist l

@[simp]

theorem List.nodup_mergeSort {α : Type u} {l : List α} {le : α → α → Bool} : (l.mergeSort le).Nodup ↔ l.Nodup

theorem List.Nodup.mergeSort {α : Type u} {l : List α} {le : α → α → Bool} : l.Nodup → (l.mergeSort le).Nodup

Alias of the reverse direction of List.nodup_mergeSort.

theorem List.nodup_iff_injective_getElem {α : Type u} {l : List α} : l.Nodup ↔ Function.Injective fun (i : Fin l.length) => l[↑i]

theorem List.nodup_iff_injective_get {α : Type u} {l : List α} : l.Nodup ↔ Function.Injective l.get

theorem List.Nodup.injective_get {α : Type u} {l : List α} (h : l.Nodup) : Function.Injective l.get

theorem Function.Injective.nodup {α : Type u} {l : List α} (h : Injective l.get) : l.Nodup

theorem List.Nodup.get_inj_iff {α : Type u} {l : List α} (h : l.Nodup) {i j : Fin l.length} : l.get i = l.get j ↔ i = j

theorem List.Nodup.getElem_inj_iff {α : Type u} {l : List α} (h : l.Nodup) {i : ℕ} {hi : i < l.length} {j : ℕ} {hj : j < l.length} : l[i] = l[j] ↔ i = j

theorem List.nodup_iff_getElem?_ne_getElem? {α : Type u} {l : List α} : l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?

theorem List.Nodup.ne_singleton_iff {α : Type u} {l : List α} (h : l.Nodup) (x : α) : l ≠ [x] ↔ l = [] ∨ ∃ (y : α), y ∈ l ∧ y ≠ x

theorem List.not_nodup_of_get_eq_of_ne {α : Type u} (xs : List α) (n m : Fin xs.length) (h : xs.get n = xs.get m) (hne : n ≠ m) : ¬xs.Nodup

theorem List.Nodup.head_eq_getLast_iff {α : Type u} {l : List α} (hne : l ≠ []) (hnd : l.Nodup) : l.head hne = l.getLast hne ↔ ∃ (x : α), l = [x]

theorem List.get_idxOf {α : Type u} [BEq α] [LawfulBEq α] {l : List α} (H : l.Nodup) (i : Fin l.length) : idxOf (l.get i) l = ↑i

theorem List.nodup_iff_count_le_one {α : Type u} [BEq α] [LawfulBEq α] {l : List α} : l.Nodup ↔ ∀ (a : α), count a l ≤ 1

theorem List.nodup_iff_count_eq_one {α : Type u} {l : List α} [BEq α] [LawfulBEq α] : l.Nodup ↔ ∀ (a : α), a ∈ l → count a l = 1

theorem List.get_bijective_iff {α : Type u} {l : List α} [BEq α] [LawfulBEq α] : Function.Bijective l.get ↔ ∀ (a : α), count a l = 1

theorem List.getElem_bijective_iff {α : Type u} {l : List α} [BEq α] [LawfulBEq α] : (Function.Bijective fun (n : Fin l.length) => l[n]) ↔ ∀ (a : α), count a l = 1

@[simp]

theorem List.count_eq_one_of_mem {α : Type u} [BEq α] [LawfulBEq α] {a : α} {l : List α} (d : l.Nodup) (h : a ∈ l) : count a l = 1

theorem List.Nodup.of_append_left {α : Type u} {l₁ l₂ : List α} : (l₁ ++ l₂).Nodup → l₁.Nodup

theorem List.Nodup.of_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₂

This is a variant of the nodup_append from the standard library, which does not use Disjoint.

theorem List.disjoint_of_nodup_append {α : Type u} {l₁ l₂ : List α} (d : (l₁ ++ l₂).Nodup) : l₁.Disjoint l₂

theorem List.Nodup.disjoint {α : Type u} {l₁ l₂ : List α} (d : (l₁ ++ l₂).Nodup) : l₁.Disjoint l₂

Alias of List.disjoint_of_nodup_append.

theorem List.Nodup.append {α : Type u} {l₁ l₂ : List α} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) (dj : l₁.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_map {α : Type u} {β : Type v} (f : α → β) {l : List α} : (map f l).Nodup → l.Nodup

theorem List.Nodup.map_on {α : Type u} {β : Type v} {l : List α} {f : α → β} (H : ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ l → f x = f y → x = y) (d : l.Nodup) : (map f l).Nodup

theorem List.inj_on_of_nodup_map {α : Type u} {β : Type v} {f : α → β} {l : List α} (d : (map f l).Nodup) ⦃x : α⦄ : x ∈ l → ∀ ⦃y : α⦄, y ∈ l → f x = f y → x = y

theorem List.nodup_map_iff_inj_on {α : Type u} {β : Type v} {f : α → β} {l : List α} (d : l.Nodup) : (map f l).Nodup ↔ ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ l → f x = f y → x = y

theorem List.Nodup.map {α : Type u} {β : Type v} {l : List α} {f : α → β} (hf : Function.Injective f) : l.Nodup → (map f l).Nodup

theorem List.nodup_map_iff {α : Type u} {β : Type v} {f : α → β} {l : List α} (hf : Function.Injective f) : (map f l).Nodup ↔ l.Nodup

@[simp]

theorem List.nodup_attach {α : Type u} {l : List α} : l.attach.Nodup ↔ l.Nodup

theorem List.Nodup.of_attach {α : Type u} {l : List α} : l.attach.Nodup → l.Nodup

Alias of the forward direction of List.nodup_attach.

theorem List.Nodup.attach {α : Type u} {l : List α} : l.Nodup → l.attach.Nodup

Alias of the reverse direction of List.nodup_attach.

theorem List.Nodup.pmap {α : Type u} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ (a : α), a ∈ l → p a} (hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b) (h : l.Nodup) : (List.pmap f l H).Nodup

theorem List.Nodup.filter {α : Type u} (p : α → Bool) {l : List α} : l.Nodup → (List.filter p l).Nodup

@[simp]

theorem List.nodup_reverse {α : Type u} {l : List α} : l.reverse.Nodup ↔ l.Nodup

theorem List.nodup_concat {α : Type u} (l : List α) (u : α) : (l.concat u).Nodup ↔ ¬u ∈ l ∧ l.Nodup

@[simp]

theorem List.Nodup.tail {α : Type u} {l : List α} (h : l.Nodup) : l.tail.Nodup

theorem List.nodup_tail_reverse {α : Type u} (l : List α) (h : l[0]? = l.getLast?) : l.reverse.tail.Nodup ↔ l.tail.Nodup

theorem List.Nodup.eq_of_head_mem_of_suffix {α : Type u} {l₁ l₂ : List α} (h : l₁ <:+ l₂) {hne : l₂ ≠ []} (hl : l₂.head hne ∈ l₁) (hnd : l₂.Nodup) : l₁ = l₂

theorem List.Nodup.eq_of_getLast_mem_of_prefix {α : Type u} {l₁ l₂ : List α} (h : l₁ <+: l₂) {hne : l₂ ≠ []} (hl : l₂.getLast hne ∈ l₁) (hnd : l₂.Nodup) : l₁ = l₂

theorem List.Nodup.prefix_of_head_mem_of_infix {α : Type u} {l₁ l₂ : List α} (h : l₁ <:+: l₂) {hne : l₂ ≠ []} (hl : l₂.head hne ∈ l₁) (hnd : l₂.Nodup) : l₁ <+: l₂

theorem List.Nodup.suffix_of_getLast_mem_of_infix {α : Type u} {l₁ l₂ : List α} (h : l₁ <:+: l₂) {hne : l₂ ≠ []} (hl : l₂.getLast hne ∈ l₁) (hnd : l₂.Nodup) : l₁ <:+ l₂

theorem List.Nodup.eq_of_head_mem_of_getLast_mem_of_infix {α : Type u} {l₁ l₂ : List α} (h : l₁ <:+: l₂) {hne : l₂ ≠ []} (hlh : l₂.head hne ∈ l₁) (hlg : l₂.getLast hne ∈ l₁) (hnd : l₂.Nodup) : l₁ = l₂

theorem List.Nodup.erase_getElem {α : Type u} [BEq α] [LawfulBEq α] {l : List α} (hl : l.Nodup) (i : ℕ) (h : i < l.length) : l.erase l[i] = l.eraseIdx i

theorem List.Nodup.erase_get {α : Type u} [BEq α] [LawfulBEq α] {l : List α} (hl : l.Nodup) (i : Fin l.length) : l.erase (l.get i) = l.eraseIdx ↑i

theorem List.Nodup.diff {α : Type u} {l₁ l₂ : List α} [BEq α] [LawfulBEq α] : l₁.Nodup → (l₁.diff l₂).Nodup

theorem List.nodup_flatten {α : Type u} {L : List (List α)} : L.flatten.Nodup ↔ (∀ (l : List α), l ∈ L → l.Nodup) ∧ Pairwise Disjoint L

theorem List.nodup_flatMap {α : Type u} {β : Type v} {l₁ : List α} {f : α → List β} : (flatMap f l₁).Nodup ↔ (∀ (x : α), x ∈ l₁ → (f x).Nodup) ∧ Pairwise (Function.onFun Disjoint f) l₁

theorem List.Nodup.product {α : Type u} {β : Type v} {l₁ : List α} {l₂ : List β} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) : (l₁ ×ˢ l₂).Nodup

theorem List.Nodup.sigma {α : Type u} {l₁ : List α} {σ : α → Type u_1} {l₂ : (a : α) → List (σ a)} (d₁ : l₁.Nodup) (d₂ : ∀ (a : α), (l₂ a).Nodup) : (l₁.sigma l₂).Nodup

theorem List.Nodup.filterMap {α : Type u} {β : Type v} {l : List α} {f : α → Option β} (h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a') : l.Nodup → (filterMap f l).Nodup

theorem List.Nodup.concat {α : Type u} {l : List α} {a : α} (h : ¬a ∈ l) (h' : l.Nodup) : (l.concat a).Nodup

theorem List.Nodup.insert {α : Type u} {l : List α} {a : α} [BEq α] [LawfulBEq α] (h : l.Nodup) : (List.insert a l).Nodup

theorem List.Nodup.union {α : Type u} {l₂ : List α} [BEq α] [LawfulBEq α] (l₁ : List α) (h : l₂.Nodup) : (l₁ ∪ l₂).Nodup

theorem List.Nodup.inter {α : Type u} {l₁ : List α} [BEq α] (l₂ : List α) : l₁.Nodup → (l₁ ∩ l₂).Nodup

theorem List.Nodup.sdiff_eq_filter {α : Type u} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.Nodup → l₁.diff l₂ = List.filter (fun (x : α) => decide ¬x ∈ l₂) l₁

@[deprecated List.Nodup.sdiff_eq_filter (since := "2026-06-03")]

theorem List.Nodup.diff_eq_filter {α : Type u} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : l₁.Nodup → l₁.diff l₂ = List.filter (fun (x : α) => decide ¬x ∈ l₂) l₁

Alias of List.Nodup.sdiff_eq_filter.

theorem List.Nodup.mem_sdiff_iff {α : Type u} {l₁ l₂ : List α} {a : α} [BEq α] [LawfulBEq α] (hl₁ : l₁.Nodup) : a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂

@[deprecated List.Nodup.mem_sdiff_iff (since := "2026-06-03")]

theorem List.Nodup.mem_diff_iff {α : Type u} {l₁ l₂ : List α} {a : α} [BEq α] [LawfulBEq α] (hl₁ : l₁.Nodup) : a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂

Alias of List.Nodup.mem_sdiff_iff.

theorem List.Nodup.set {α : Type u} {l : List α} {n : ℕ} {a : α} : l.Nodup → ¬a ∈ l → (l.set n a).Nodup

theorem List.Nodup.map_update {α : Type u} {β : Type v} [DecidableEq α] {l : List α} (hl : l.Nodup) (f : α → β) (x : α) (y : β) : map (Function.update f x y) l = if x ∈ l then (map f l).set (idxOf x l) y else map f l

theorem List.Nodup.pairwise_of_forall_ne {α : Type u} {l : List α} {r : α → α → Prop} (hl : l.Nodup) (h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b) : Pairwise r l

theorem List.Nodup.take_eq_filter_mem {α : Type u} [BEq α] [LawfulBEq α] {l : List α} {n : ℕ} : l.Nodup → take n l = List.filter (fun (a : α) => elem a (take n l)) l

theorem Option.toList_nodup {α : Type u} (o : Option α) : o.toList.Nodup