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}
[IsIrrefl α r]
(h : List.Pairwise r l)
:
l.Nodup
theorem
List.rel_nodup
{α : Type u}
{β : Type v}
{r : α → β → Prop}
(hr : Relator.BiUnique r)
:
(List.Forall₂ r ⇒ fun (x x_1 : Prop) => x ↔ x_1) List.Nodup List.Nodup
theorem
List.Nodup.cons
{α : Type u}
{l : List α}
{a : α}
(ha : a ∉ l)
(hl : l.Nodup)
:
(a :: l).Nodup
theorem
List.Nodup.sublist
{α : Type u}
{l₁ : List α}
{l₂ : List α}
:
l₁.Sublist l₂ → l₂.Nodup → l₁.Nodup
theorem
List.nodup_iff_injective_getElem
{α : Type u}
{l : List α}
:
l.Nodup ↔ Function.Injective fun (i : Fin l.length) => l[↑i]
theorem
List.indexOf_getElem
{α : Type u}
[DecidableEq α]
{l : List α}
(H : l.Nodup)
(i : ℕ)
(h : i < l.length)
:
List.indexOf l[i] l = i
theorem
List.get_indexOf
{α : Type u}
[DecidableEq α]
{l : List α}
(H : l.Nodup)
(i : Fin l.length)
:
List.indexOf (l.get i) l = ↑i
theorem
List.nodup_iff_count_le_one
{α : Type u}
[DecidableEq α]
{l : List α}
:
l.Nodup ↔ ∀ (a : α), List.count a l ≤ 1
theorem
List.nodup_iff_count_eq_one
{α : Type u}
{l : List α}
[DecidableEq α]
:
l.Nodup ↔ ∀ a ∈ l, List.count a l = 1
@[simp]
theorem
List.count_eq_one_of_mem
{α : Type u}
[DecidableEq α]
{a : α}
{l : List α}
(d : l.Nodup)
(h : a ∈ l)
:
List.count a l = 1
theorem
List.count_eq_of_nodup
{α : Type u}
[DecidableEq α]
{a : α}
{l : List α}
(d : l.Nodup)
:
List.count a l = if a ∈ l then 1 else 0
theorem
List.Nodup.map
{α : Type u}
{β : Type v}
{l : List α}
{f : α → β}
(hf : Function.Injective f)
:
l.Nodup → (List.map f l).Nodup
theorem
List.nodup_map_iff
{α : Type u}
{β : Type v}
{f : α → β}
{l : List α}
(hf : Function.Injective f)
:
Alias of the forward direction of List.nodup_attach.
Alias of the reverse direction of List.nodup_attach.
theorem
List.Nodup.filter
{α : Type u}
(p : α → Bool)
{l : List α}
:
l.Nodup → (List.filter p l).Nodup
theorem
List.Nodup.erase_eq_filter
{α : Type u}
[DecidableEq α]
{l : List α}
(d : l.Nodup)
(a : α)
:
l.erase a = List.filter (fun (x : α) => decide (x ≠ a)) l
theorem
List.Nodup.erase
{α : Type u}
{l : List α}
[DecidableEq α]
(a : α)
:
l.Nodup → (l.erase a).Nodup
theorem
List.Nodup.erase_getElem
{α : Type u}
[DecidableEq α]
{l : List α}
(hl : l.Nodup)
(i : ℕ)
(h : i < l.length)
:
l.erase l[i] = l.eraseIdx i
theorem
List.Nodup.erase_get
{α : Type u}
[DecidableEq α]
{l : List α}
(hl : l.Nodup)
(i : Fin l.length)
:
l.erase (l.get i) = l.eraseIdx ↑i
theorem
List.Nodup.diff
{α : Type u}
{l₁ : List α}
{l₂ : List α}
[DecidableEq α]
:
l₁.Nodup → (l₁.diff l₂).Nodup
theorem
List.Nodup.mem_erase_iff
{α : Type u}
{l : List α}
{a : α}
{b : α}
[DecidableEq α]
(d : l.Nodup)
:
theorem
List.Nodup.not_mem_erase
{α : Type u}
{l : List α}
{a : α}
[DecidableEq α]
(h : l.Nodup)
:
a ∉ l.erase a
theorem
List.nodup_join
{α : Type u}
{L : List (List α)}
:
L.join.Nodup ↔ (∀ 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 ∈ l₁, (f x).Nodup) ∧ List.Pairwise (fun (a b : α) => (f a).Disjoint (f b)) l₁
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 → (List.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 : α}
[DecidableEq α]
(h : l.Nodup)
:
(List.insert a l).Nodup
theorem
List.Nodup.union
{α : Type u}
{l₂ : List α}
[DecidableEq α]
(l₁ : List α)
(h : l₂.Nodup)
:
(l₁ ∪ l₂).Nodup
theorem
List.Nodup.inter
{α : Type u}
{l₁ : List α}
[DecidableEq α]
(l₂ : List α)
:
l₁.Nodup → (l₁ ∩ l₂).Nodup
theorem
List.Nodup.diff_eq_filter
{α : Type u}
[DecidableEq α]
{l₁ : List α}
{l₂ : List α}
:
l₁.Nodup → l₁.diff l₂ = List.filter (fun (x : α) => decide (x ∉ l₂)) l₁
theorem
List.Nodup.mem_diff_iff
{α : Type u}
{l₁ : List α}
{l₂ : List α}
{a : α}
[DecidableEq α]
(hl₁ : l₁.Nodup)
:
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 : β)
:
List.map (Function.update f x y) l = if x ∈ l then (List.map f l).set (List.indexOf x l) y else List.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)
:
List.Pairwise r l
theorem
List.Nodup.pairwise_of_set_pairwise
{α : Type u}
{l : List α}
{r : α → α → Prop}
(hl : l.Nodup)
(h : {x : α | x ∈ l}.Pairwise r)
:
List.Pairwise r l
@[simp]
theorem
List.Nodup.pairwise_coe
{α : Type u}
{l : List α}
{r : α → α → Prop}
[IsSymm α r]
(hl : l.Nodup)
:
{a : α | a ∈ l}.Pairwise r ↔ List.Pairwise r l
theorem
List.Nodup.take_eq_filter_mem
{α : Type u}
[DecidableEq α]
{l : List α}
{n : ℕ}
:
l.Nodup → List.take n l = List.filter (fun (a : α) => List.elem a (List.take n l)) l