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
@[deprecated List.Pairwise.nodup (since := "2025-10-11")]
theorem
List.Sorted.nodup
{α : Type u}
{l : List α}
{r : α → α → Prop}
[Std.Irrefl r]
(h : Pairwise r l)
:
l.Nodup
Alias of List.Pairwise.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
@[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.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.ne_singleton_iff
{α : Type u}
{l : List α}
(h : l.Nodup)
(x : α)
:
l ≠ [x] ↔ l = [] ∨ ∃ 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
@[deprecated List.Nodup.idxOf_getElem (since := "2025-11-10")]
theorem
List.idxOf_getElem
{α : Type u}
[DecidableEq α]
{l : List α}
:
l.Nodup → ∀ (i : ℕ) (h : i < l.length), idxOf l[i] l = i
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 ∈ 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
@[deprecated List.Nodup.count (since := "2025-11-07")]
theorem
List.count_eq_of_nodup
{α : Type u_1}
[BEq α]
[LawfulBEq α]
{a : α}
{l : List α}
(h : l.Nodup)
:
count a l = if a ∈ l then 1 else 0
Alias of List.Nodup.count.
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₂
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_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 ∈ l, ∀ 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 ∈ l, ∀ 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
Alias of the reverse direction of List.nodup_attach.
Alias of the forward direction of List.nodup_attach.
theorem
List.Nodup.pmap
{α : Type u}
{β : Type v}
{p : α → Prop}
{f : (a : α) → p a → β}
{l : List α}
{H : ∀ 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
theorem
List.nodup_tail_reverse
{α : Type u}
(l : List α)
(h : l[0]? = l.getLast?)
:
l.reverse.tail.Nodup ↔ l.tail.Nodup
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 ∈ L, l.Nodup) ∧ Pairwise Disjoint L
theorem
List.nodup_flatMap
{α : Type u}
{β : Type v}
{l₁ : List α}
{f : α → List β}
:
(flatMap f l₁).Nodup ↔ (∀ 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 ∈ 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.diff_eq_filter
{α : Type u}
[BEq α]
[LawfulBEq α]
{l₁ l₂ : List α}
:
l₁.Nodup → l₁.diff l₂ = List.filter (fun (x : α) => decide (x ∉ l₂)) l₁
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₂
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 ∈ l, ∀ 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