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} : List.Nodup []

@[simp]

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

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

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

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

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

theorem List.Nodup.of_cons {α : Type u} {l : List α} {a : α} (h : List.Nodup (a :: l)) : List.Nodup 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₂ → List.Nodup l₂ → List.Nodup l₁

theorem List.not_nodup_pair {α : Type u} (a : α) : ¬List.Nodup [a, a]

theorem List.nodup_iff_sublist {α : Type u} {l : List α} : List.Nodup l ↔ ∀ (a : α), ¬List.Sublist [a, a] l

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

@[deprecated List.nodup_iff_injective_get]

theorem List.nodup_iff_nthLe_inj {α : Type u} {l : List α} : List.Nodup l ↔ ∀ (i j : ℕ) (h₁ : i < List.length l) (h₂ : j < List.length l), List.nthLe l i h₁ = List.nthLe l j h₂ → i = j

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

@[deprecated List.Nodup.get_inj_iff]

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

theorem List.nodup_iff_get?_ne_get? {α : Type u} {l : List α} : List.Nodup l ↔ ∀ (i j : ℕ), i < j → j < List.length l → List.get? l i ≠ List.get? l j

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

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

@[deprecated List.not_nodup_of_get_eq_of_ne]

theorem List.nthLe_eq_of_ne_imp_not_nodup {α : Type u} (xs : List α) (n : ℕ) (m : ℕ) (hn : n < List.length xs) (hm : m < List.length xs) (h : List.nthLe xs n hn = List.nthLe xs m hm) (hne : n ≠ m) : ¬List.Nodup xs

theorem List.get_indexOf {α : Type u} [DecidableEq α] {l : List α} (H : List.Nodup l) (i : Fin (List.length l)) : List.indexOf (List.get l i) l = ↑i

@[simp, deprecated List.get_indexOf]

theorem List.nthLe_index_of {α : Type u} [DecidableEq α] {l : List α} (H : List.Nodup l) (n : ℕ) (h : n < List.length l) : List.indexOf (List.nthLe l n h) l = n

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

theorem List.nodup_replicate {α : Type u} (a : α) {n : ℕ} : List.Nodup (List.replicate n a) ↔ n ≤ 1

@[simp]

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

theorem List.count_eq_of_nodup {α : Type u} [DecidableEq α] {a : α} {l : List α} (d : List.Nodup l) : List.count a l = if a ∈ l then 1 else 0

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

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

theorem List.nodup_append {α : Type u} {l₁ : List α} {l₂ : List α} : List.Nodup (l₁ ++ l₂) ↔ List.Nodup l₁ ∧ List.Nodup 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₁ : List.Nodup l₁) (d₂ : List.Nodup l₂) (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) → List.Nodup l

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 : List.Nodup l) : List.Nodup (List.map f l)

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 ∈ l → f x = f y → x = y

theorem List.nodup_map_iff_inj_on {α : Type u} {β : Type v} {f : α → β} {l : List α} (d : List.Nodup l) : List.Nodup (List.map f l) ↔ ∀ (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) : List.Nodup l → List.Nodup (List.map f l)

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

@[simp]

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

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

Alias of the reverse direction of List.nodup_attach.

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

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 ∈ l → p a} (hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b) (h : List.Nodup l) : List.Nodup (List.pmap f l H)

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

@[simp]

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

theorem List.Nodup.erase_eq_filter {α : Type u} [DecidableEq α] {l : List α} (d : List.Nodup l) (a : α) : List.erase l a = List.filter (fun x => decide (x ≠ a)) l

theorem List.Nodup.erase {α : Type u} {l : List α} [DecidableEq α] (a : α) : List.Nodup l → List.Nodup (List.erase l a)

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

theorem List.Nodup.mem_erase_iff {α : Type u} {l : List α} {a : α} {b : α} [DecidableEq α] (d : List.Nodup l) : a ∈ List.erase l b ↔ a ≠ b ∧ a ∈ l

theorem List.Nodup.not_mem_erase {α : Type u} {l : List α} {a : α} [DecidableEq α] (h : List.Nodup l) : ¬a ∈ List.erase l a

theorem List.nodup_join {α : Type u} {L : List (List α)} : List.Nodup (List.join L) ↔ (∀ (l : List α), l ∈ L → List.Nodup 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₁ : List.Nodup l₁) (d₂ : List.Nodup l₂) : List.Nodup (l₁ ×ˢ l₂)

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

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

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

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

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

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

theorem List.Nodup.diff_eq_filter {α : Type u} [DecidableEq α] {l₁ : List α} {l₂ : List α} : List.Nodup l₁ → 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 : α} [DecidableEq α] (hl₁ : List.Nodup l₁) : a ∈ List.diff l₁ l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂

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

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

theorem List.Nodup.pairwise_of_forall_ne {α : Type u} {l : List α} {r : α → α → Prop} (hl : List.Nodup l) (h : (a : α) → a ∈ l → (b : α) → 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 : List.Nodup l) (h : Set.Pairwise {x | x ∈ l} r) : List.Pairwise r l

@[simp]

theorem List.Nodup.pairwise_coe {α : Type u} {l : List α} {r : α → α → Prop} [IsSymm α r] (hl : List.Nodup l) : Set.Pairwise {a | a ∈ l} r ↔ List.Pairwise r l

theorem List.Nodup.take_eq_filter_mem {α : Type u} [DecidableEq α] {l : List α} {n : ℕ} : List.Nodup l → List.take n l = List.filter (fun x => decide (x ∈ List.take n l)) l

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