# Documentation

Mathlib.Data.List.Nodup

# Lists with no duplicates #

List.Nodup is defined in Data/List/Basic. 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 α} :
theorem List.Pairwise.nodup {α : Type u} {l : List α} {r : ααProp} [inst : IsIrrefl α r] (h : ) :
theorem List.rel_nodup {α : Type u} {β : Type v} {r : αβProp} (hr : ) :
fun x x_1 => x x_1) List.Nodup List.Nodup
theorem List.Nodup.cons {α : Type u} {l : List α} {a : α} (ha : ¬a l) (hl : ) :
theorem List.nodup_singleton {α : Type u} (a : α) :
theorem List.Nodup.of_cons {α : Type u} {l : List α} {a : α} (h : List.Nodup (a :: l)) :
theorem List.Nodup.not_mem {α : Type u} {l : List α} {a : α} (h : List.Nodup (a :: l)) :
¬a l
theorem List.not_nodup_cons_of_mem {α : Type u} {l : List α} {a : α} :
a l¬List.Nodup (a :: l)
theorem List.Nodup.sublist {α : Type u} {l₁ : List α} {l₂ : List α} :
List.Sublist l₁ l₂
theorem List.not_nodup_pair {α : Type u} (a : α) :
theorem List.nodup_iff_sublist {α : Type u} {l : List α} :
∀ (a : α), ¬List.Sublist [a, a] l
theorem List.nodup_iff_injective_get {α : Type u} {l : List α} :
theorem List.nodup_iff_nthLe_inj {α : Type u} {l : List α} :
∀ (i j : ) (h₁ : i < ) (h₂ : j < ), List.nthLe l i h₁ = List.nthLe l j h₂i = j
theorem List.Nodup.get_inj_iff {α : Type u} {l : List α} (h : ) {i : Fin ()} {j : Fin ()} :
List.get l i = List.get l j i = j
theorem List.Nodup.nthLe_inj_iff {α : Type u} {l : List α} (h : ) {i : } {j : } (hi : i < ) (hj : j < ) :
List.nthLe l i hi = List.nthLe l j hj i = j
theorem List.nodup_iff_get?_ne_get? {α : Type u} {l : List α} :
∀ (i j : ), i < jj <
theorem List.Nodup.ne_singleton_iff {α : Type u} {l : List α} (h : ) (x : α) :
l [x] l = [] y, y l y x
theorem List.not_nodup_of_get_eq_of_ne {α : Type u} (xs : List α) (n : Fin ()) (m : Fin ()) (h : List.get xs n = List.get xs m) (hne : n m) :
theorem List.nthLe_eq_of_ne_imp_not_nodup {α : Type u} (xs : List α) (n : ) (m : ) (hn : n < ) (hm : m < ) (h : List.nthLe xs n hn = List.nthLe xs m hm) (hne : n m) :
theorem List.get_indexOf {α : Type u} [inst : ] {l : List α} (H : ) (i : Fin ()) :
List.indexOf (List.get l i) l = i
@[simp]
theorem List.nthLe_index_of {α : Type u} [inst : ] {l : List α} (H : ) (n : ) (h : n < ) :
theorem List.nodup_iff_count_le_one {α : Type u} [inst : ] {l : List α} :
∀ (a : α), 1
theorem List.nodup_replicate {α : Type u} (a : α) {n : } :
@[simp]
theorem List.count_eq_one_of_mem {α : Type u} [inst : ] {a : α} {l : List α} (d : ) (h : a l) :
= 1
theorem List.count_eq_of_nodup {α : Type u} [inst : ] {a : α} {l : List α} (d : ) :
= if a l then 1 else 0
theorem List.Nodup.of_append_left {α : Type u} {l₁ : List α} {l₂ : List α} :
List.Nodup (l₁ ++ l₂)
theorem List.Nodup.of_append_right {α : Type u} {l₁ : List α} {l₂ : List α} :
List.Nodup (l₁ ++ l₂)
theorem List.nodup_append {α : Type u} {l₁ : List α} {l₂ : List α} :
List.Nodup (l₁ ++ l₂) List.Disjoint l₁ l₂
theorem List.disjoint_of_nodup_append {α : Type u} {l₁ : List α} {l₂ : List α} (d : List.Nodup (l₁ ++ l₂)) :
List.Disjoint l₁ l₂
theorem List.Nodup.append {α : Type u} {l₁ : List α} {l₂ : List α} (d₁ : ) (d₂ : ) (dj : List.Disjoint l₁ l₂) :
List.Nodup (l₁ ++ l₂)
theorem List.nodup_append_comm {α : Type u} {l₁ : List α} {l₂ : List α} :
List.Nodup (l₁ ++ l₂) List.Nodup (l₂ ++ l₁)
theorem List.nodup_middle {α : Type u} {a : α} {l₁ : List α} {l₂ : List α} :
List.Nodup (l₁ ++ a :: l₂) List.Nodup (a :: (l₁ ++ l₂))
theorem List.Nodup.of_map {α : Type u} {β : Type v} (f : αβ) {l : List α} :
List.Nodup (List.map f l)
theorem List.Nodup.map_on {α : Type u} {β : Type v} {l : List α} {f : αβ} (H : ∀ (x : α), x l∀ (y : α), y lf x = f yx = y) (d : ) :
theorem List.inj_on_of_nodup_map {α : Type u} {β : Type v} {f : αβ} {l : List α} (d : List.Nodup (List.map f l)) ⦃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 : ) :
List.Nodup (List.map f l) ∀ (x : α), x l∀ (y : α), y lf x = f yx = y
theorem List.Nodup.map {α : Type u} {β : Type v} {l : List α} {f : αβ} (hf : ) :
List.Nodup (List.map f l)
theorem List.nodup_map_iff {α : Type u} {β : Type v} {f : αβ} {l : List α} (hf : ) :
@[simp]
theorem List.nodup_attach {α : Type u} {l : List α} :
theorem List.Nodup.attach {α : Type u} {l : List α} :

Alias of the reverse direction of List.nodup_attach.

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

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 : α) → a lp a} (hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hba = b) (h : ) :
theorem List.Nodup.filter {α : Type u} (p : αBool) {l : List α} :
List.Nodup ()
@[simp]
theorem List.nodup_reverse {α : Type u} {l : List α} :
theorem List.Nodup.erase_eq_filter {α : Type u} [inst : ] {l : List α} (d : ) (a : α) :
= List.filter (fun x => decide (x a)) l
theorem List.Nodup.erase {α : Type u} {l : List α} [inst : ] (a : α) :
List.Nodup ()
theorem List.Nodup.diff {α : Type u} {l₁ : List α} {l₂ : List α} [inst : ] :
List.Nodup (List.diff l₁ l₂)
theorem List.Nodup.mem_erase_iff {α : Type u} {l : List α} {a : α} {b : α} [inst : ] (d : ) :
a a b a l
theorem List.Nodup.not_mem_erase {α : Type u} {l : List α} {a : α} [inst : ] (h : ) :
theorem List.nodup_join {α : Type u} {L : List (List α)} :
(∀ (l : List α), l L) List.Pairwise List.Disjoint L
theorem List.nodup_bind {α : Type u} {β : Type v} {l₁ : List α} {f : αList β} :
List.Nodup (List.bind l₁ f) (∀ (x : α), x l₁List.Nodup (f x)) List.Pairwise (fun a b => List.Disjoint (f a) (f b)) l₁
theorem List.Nodup.product {α : Type u} {β : Type v} {l₁ : List α} {l₂ : List β} (d₁ : ) (d₂ : ) :
List.Nodup (l₁ ×ˢ l₂)
theorem List.Nodup.sigma {α : Type u} {l₁ : List α} {σ : αType u_1} {l₂ : (a : α) → List (σ a)} (d₁ : ) (d₂ : ∀ (a : α), List.Nodup (l₂ a)) :
theorem List.Nodup.filterMap {α : Type u} {β : Type v} {l : List α} {f : α} (h : ∀ (a a' : α) (b : β), b f ab f a'a = a') :
List.Nodup ()
theorem List.Nodup.concat {α : Type u} {l : List α} {a : α} (h : ¬a l) (h' : ) :
theorem List.Nodup.insert {α : Type u} {l : List α} {a : α} [inst : ] (h : ) :
theorem List.Nodup.union {α : Type u} {l₂ : List α} [inst : ] (l₁ : List α) (h : ) :
List.Nodup (l₁ l₂)
theorem List.Nodup.inter {α : Type u} {l₁ : List α} [inst : ] (l₂ : List α) :
List.Nodup (l₁ l₂)
theorem List.Nodup.diff_eq_filter {α : Type u} [inst : ] {l₁ : List α} {l₂ : List α} :
List.diff l₁ l₂ = List.filter (fun x => decide ¬x l₂) l₁
theorem List.Nodup.mem_diff_iff {α : Type u} {l₁ : List α} {l₂ : List α} {a : α} [inst : ] (hl₁ : ) :
a List.diff l₁ l₂ a l₁ ¬a l₂
theorem List.Nodup.set {α : Type u} {l : List α} {n : } {a : α} :
¬a lList.Nodup (List.set l n a)
theorem List.Nodup.map_update {α : Type u} {β : Type v} [inst : ] {l : List α} (hl : ) (f : αβ) (x : α) (y : β) :
List.map () l = if x l then List.set (List.map f l) () y else List.map f l
theorem List.Nodup.pairwise_of_forall_ne {α : Type u} {l : List α} {r : ααProp} (hl : ) (h : (a : α) → a l(b : α) → b la br a b) :
theorem List.Nodup.pairwise_of_set_pairwise {α : Type u} {l : List α} {r : ααProp} (hl : ) (h : Set.Pairwise { x | x l } r) :
@[simp]
theorem List.Nodup.pairwise_coe {α : Type u} {l : List α} {r : ααProp} [inst : IsSymm α r] (hl : ) :
Set.Pairwise { a | a l } r
theorem List.Nodup.take_eq_filter_mem {α : Type u} [inst : ] {l : List α} {n : } :
= List.filter (fun x => decide (x )) l
theorem Option.toList_nodup {α : Type u_1} (o : ) :