# 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 : ) :
l.Nodup
theorem List.rel_nodup {α : Type u} {β : Type v} {r : αβProp} (hr : ) :
( fun (x1 x2 : Prop) => x1 x2) List.Nodup List.Nodup
theorem List.Nodup.cons {α : Type u} {l : List α} {a : α} (ha : al) (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.not_mem {α : Type u} {l : List α} {a : α} (h : (a :: l).Nodup) :
al
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
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.get_inj_iff {α : Type u} {l : List α} (h : l.Nodup) {i : Fin l.length} {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 < jj < l.lengthl[i]? l[j]?
theorem List.nodup_iff_get?_ne_get? {α : Type u} {l : List α} :
l.Nodup ∀ (i j : ), i < jj < l.lengthl.get? i l.get? j
theorem List.Nodup.ne_singleton_iff {α : Type u} {l : List α} (h : l.Nodup) (x : α) :
l [x] l = [] yl, y x
theorem List.not_nodup_of_get_eq_of_ne {α : Type u} (xs : List α) (n : Fin xs.length) (m : Fin xs.length) (h : xs.get n = xs.get m) (hne : n m) :
¬xs.Nodup
theorem List.indexOf_getElem {α : Type u} [] {l : List α} (H : l.Nodup) (i : ) (h : i < l.length) :
List.indexOf l[i] l = i
theorem List.get_indexOf {α : Type u} [] {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} [] {l : List α} :
l.Nodup ∀ (a : α), 1
theorem List.nodup_iff_count_eq_one {α : Type u} {l : List α} [] :
l.Nodup al, = 1
@[simp]
theorem List.count_eq_one_of_mem {α : Type u} [] {a : α} {l : List α} (d : l.Nodup) (h : a l) :
= 1
theorem List.count_eq_of_nodup {α : Type u} [] {a : α} {l : List α} (d : l.Nodup) :
= if a l then 1 else 0
theorem List.Nodup.of_append_left {α : Type u} {l₁ : List α} {l₂ : List α} :
(l₁ ++ l₂).Nodupl₁.Nodup
theorem List.Nodup.of_append_right {α : Type u} {l₁ : List α} {l₂ : List α} :
(l₁ ++ l₂).Nodupl₂.Nodup
theorem List.nodup_append {α : Type u} {l₁ : List α} {l₂ : List α} :
(l₁ ++ l₂).Nodup l₁.Nodup l₂.Nodup l₁.Disjoint l₂
theorem List.disjoint_of_nodup_append {α : Type u} {l₁ : List α} {l₂ : List α} (d : (l₁ ++ l₂).Nodup) :
l₁.Disjoint l₂
theorem List.Nodup.append {α : Type u} {l₁ : List α} {l₂ : List α} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) (dj : l₁.Disjoint l₂) :
(l₁ ++ l₂).Nodup
theorem List.nodup_append_comm {α : Type u} {l₁ : List α} {l₂ : List α} :
(l₁ ++ l₂).Nodup (l₂ ++ l₁).Nodup
theorem List.nodup_middle {α : Type u} {a : α} {l₁ : List α} {l₂ : List α} :
(l₁ ++ a :: l₂).Nodup (a :: (l₁ ++ l₂)).Nodup
theorem List.Nodup.of_map {α : Type u} {β : Type v} (f : αβ) {l : List α} :
(List.map f l).Nodupl.Nodup
theorem List.Nodup.map_on {α : Type u} {β : Type v} {l : List α} {f : αβ} (H : xl, yl, f x = f yx = y) (d : l.Nodup) :
(List.map f l).Nodup
theorem List.inj_on_of_nodup_map {α : Type u} {β : Type v} {f : αβ} {l : List α} (d : (List.map f l).Nodup) ⦃x : α :
x l∀ ⦃y : α⦄, y lf x = f yx = y
theorem List.nodup_map_iff_inj_on {α : Type u} {β : Type v} {f : αβ} {l : List α} (d : l.Nodup) :
(List.map f l).Nodup xl, yl, f x = f yx = y
theorem List.Nodup.map {α : Type u} {β : Type v} {l : List α} {f : αβ} (hf : ) :
l.Nodup(List.map f l).Nodup
theorem List.nodup_map_iff {α : Type u} {β : Type v} {f : αβ} {l : List α} (hf : ) :
(List.map f l).Nodup l.Nodup
@[simp]
theorem List.nodup_attach {α : Type u} {l : List α} :
l.attach.Nodup l.Nodup
theorem List.Nodup.attach {α : Type u} {l : List α} :
l.Nodupl.attach.Nodup

Alias of the reverse direction of List.nodup_attach.

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

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 : al, p a} (hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hba = 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.erase_getElem {α : Type u} [] {l : List α} (hl : l.Nodup) (i : ) (h : i < l.length) :
l.erase l[i] = l.eraseIdx i
theorem List.Nodup.erase_get {α : Type u} [] {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 α} [] :
l₁.Nodup(l₁.diff l₂).Nodup
theorem List.nodup_join {α : Type u} {L : List (List α)} :
L.join.Nodup (∀ lL, l.Nodup) List.Pairwise List.Disjoint L
theorem List.nodup_bind {α : Type u} {β : Type v} {l₁ : List α} {f : αList β} :
(l₁.bind f).Nodup (∀ xl₁, (f x).Nodup) List.Pairwise (fun (a b : α) => (f a).Disjoint (f b)) 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 : α} (h : ∀ (a a' : α), bf a, b f a'a = a') :
l.Nodup(List.filterMap f l).Nodup
theorem List.Nodup.concat {α : Type u} {l : List α} {a : α} (h : al) (h' : l.Nodup) :
(l.concat a).Nodup
theorem List.Nodup.insert {α : Type u} {l : List α} {a : α} [] (h : l.Nodup) :
(List.insert a l).Nodup
theorem List.Nodup.union {α : Type u} {l₂ : List α} [] (l₁ : List α) (h : l₂.Nodup) :
(l₁ l₂).Nodup
theorem List.Nodup.inter {α : Type u} {l₁ : List α} [] (l₂ : List α) :
l₁.Nodup(l₁ l₂).Nodup
theorem List.Nodup.diff_eq_filter {α : Type u} [] {l₁ : List α} {l₂ : List α} :
l₁.Nodupl₁.diff l₂ = List.filter (fun (x : α) => decide (xl₂)) l₁
theorem List.Nodup.mem_diff_iff {α : Type u} {l₁ : List α} {l₂ : List α} {a : α} [] (hl₁ : l₁.Nodup) :
a l₁.diff l₂ a l₁ al₂
theorem List.Nodup.set {α : Type u} {l : List α} {n : } {a : α} :
l.Nodupal(l.set n a).Nodup
theorem List.Nodup.map_update {α : Type u} {β : Type v} [] {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 : al, bl, a br a b) :
theorem List.Nodup.pairwise_of_set_pairwise {α : Type u} {l : List α} {r : ααProp} (hl : l.Nodup) (h : {x : α | x l}.Pairwise r) :
@[simp]
theorem List.Nodup.pairwise_coe {α : Type u} {l : List α} {r : ααProp} [IsSymm α r] (hl : l.Nodup) :
{a : α | a l}.Pairwise r
theorem List.Nodup.take_eq_filter_mem {α : Type u} [] {l : List α} {n : } :
l.Nodup = List.filter (fun (a : α) => List.elem a (List.take n l)) l
theorem Option.toList_nodup {α : Type u} (o : ) :
o.toList.Nodup