mathlib3 documentation

data.list.nodup

Lists with no duplicates #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

list.nodup is defined in data/list/defs. In this file we prove various properties of this predicate.

source
@[simp]
theorem list.forall_mem_ne {α : Type u} {a : α} {l : list α} :
(∀ (a' : α), a' ∈ l → ¬a = a') ↔ a ∉ l
source
@[simp]
theorem list.nodup_nil {α : Type u} :
list.nil.nodup
source
@[simp]
theorem list.nodup_cons {α : Type u} {a : α} {l : list α} :
(a :: l).nodup ↔ a ∉ l ∧ l.nodup
source
@[protected]
theorem list.pairwise.nodup {α : Type u} {l : list α} {r : α → α → Prop} [is_irrefl α r] (h : list.pairwise r l) :
l.nodup
source
theorem list.rel_nodup {α : Type u} {β : Type v} {r : α → β → Prop} (hr : relator.bi_unique r) :
(list.forall₂ r ⇒ iff) list.nodup list.nodup
source
@[protected]
theorem list.nodup.cons {α : Type u} {l : list α} {a : α} (ha : a ∉ l) (hl : l.nodup) :
(a :: l).nodup
source
theorem list.nodup_singleton {α : Type u} (a : α) :
[a].nodup
source
theorem list.nodup.of_cons {α : Type u} {l : list α} {a : α} (h : (a :: l).nodup) :
l.nodup
source
theorem list.nodup.not_mem {α : Type u} {l : list α} {a : α} (h : (a :: l).nodup) :
a ∉ l
source
theorem list.not_nodup_cons_of_mem {α : Type u} {l : list α} {a : α} :
a ∈ l → ¬(a :: l).nodup
source
@[protected]
theorem list.nodup.sublist {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂ → l₂.nodup → l₁.nodup
source
theorem list.not_nodup_pair {α : Type u} (a : α) :
¬[a, a].nodup
source
theorem list.nodup_iff_sublist {α : Type u} {l : list α} :
l.nodup ↔ ∀ (a : α), ¬[a, a] <+ l
source
theorem list.nodup_iff_nth_le_inj {α : Type u} {l : list α} :
l.nodup ↔ ∀ (i j : ℕ) (h₁ : i < l.length) (h₂ : j < l.length), l.nth_le i h₁ = l.nth_le j h₂ → i = j
source
theorem list.nodup.nth_le_inj_iff {α : Type u} {l : list α} (h : l.nodup) {i j : ℕ} (hi : i < l.length) (hj : j < l.length) :
l.nth_le i hi = l.nth_le j hj ↔ i = j
source
theorem list.nodup_iff_nth_ne_nth {α : Type u} {l : list α} :
l.nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l.nth i ≠ l.nth j
source
theorem list.nodup.ne_singleton_iff {α : Type u} {l : list α} (h : l.nodup) (x : α) :
l ≠ [x] ↔ l = list.nil ∨ ∃ (y : α) (H : y ∈ l), y ≠ x
source
theorem list.nth_le_eq_of_ne_imp_not_nodup {α : Type u} (xs : list α) (n m : ℕ) (hn : n < xs.length) (hm : m < xs.length) (h : xs.nth_le n hn = xs.nth_le m hm) (hne : n ≠ m) :
¬xs.nodup
source
@[simp]
theorem list.nth_le_index_of {α : Type u} [decidable_eq α] {l : list α} (H : l.nodup) (n : ℕ) (h : n < l.length) :
list.index_of (l.nth_le n h) l = n
source
theorem list.nodup_iff_count_le_one {α : Type u} [decidable_eq α] {l : list α} :
l.nodup ↔ ∀ (a : α), list.count a l ≤ 1
source
theorem list.nodup_replicate {α : Type u} (a : α) {n : ℕ} :
(list.replicate n a).nodup ↔ n ≤ 1
source
@[simp]
theorem list.count_eq_one_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} (d : l.nodup) (h : a ∈ l) :
list.count a l = 1
source
theorem list.count_eq_of_nodup {α : Type u} [decidable_eq α] {a : α} {l : list α} (d : l.nodup) :
list.count a l = ite (a ∈ l) 1 0
source
theorem list.nodup.of_append_left {α : Type u} {l₁ l₂ : list α} :
(l₁ ++ l₂).nodup → l₁.nodup
source
theorem list.nodup.of_append_right {α : Type u} {l₁ l₂ : list α} :
(l₁ ++ l₂).nodup → l₂.nodup
source
theorem list.nodup_append {α : Type u} {l₁ l₂ : list α} :
(l₁ ++ l₂).nodup ↔ l₁.nodup ∧ l₂.nodup ∧ l₁.disjoint l₂
source
theorem list.disjoint_of_nodup_append {α : Type u} {l₁ l₂ : list α} (d : (l₁ ++ l₂).nodup) :
l₁.disjoint l₂
source
theorem list.nodup.append {α : Type u} {l₁ l₂ : list α} (d₁ : l₁.nodup) (d₂ : l₂.nodup) (dj : l₁.disjoint l₂) :
(l₁ ++ l₂).nodup
source
theorem list.nodup_append_comm {α : Type u} {l₁ l₂ : list α} :
(l₁ ++ l₂).nodup ↔ (l₂ ++ l₁).nodup
source
theorem list.nodup_middle {α : Type u} {a : α} {l₁ l₂ : list α} :
(l₁ ++ a :: l₂).nodup ↔ (a :: (l₁ ++ l₂)).nodup
source
theorem list.nodup.of_map {α : Type u} {β : Type v} (f : α → β) {l : list α} :
(list.map f l).nodup → l.nodup
source
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 : l.nodup) :
(list.map f l).nodup
source
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 ∈ l → f x = f y → x = y
source
theorem list.nodup_map_iff_inj_on {α : Type u} {β : Type v} {f : α → β} {l : list α} (d : l.nodup) :
(list.map f l).nodup ↔ ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ l → f x = f y → x = y
source
@[protected]
theorem list.nodup.map {α : Type u} {β : Type v} {l : list α} {f : α → β} (hf : function.injective f) :
l.nodup → (list.map f l).nodup
source
theorem list.nodup_map_iff {α : Type u} {β : Type v} {f : α → β} {l : list α} (hf : function.injective f) :
(list.map f l).nodup ↔ l.nodup
source
@[simp]
theorem list.nodup_attach {α : Type u} {l : list α} :
l.attach.nodup ↔ l.nodup
source
theorem list.nodup.of_attach {α : Type u} {l : list α} :
l.attach.nodup → l.nodup

Alias of the forward direction of list.nodup_attach.

source
@[protected]
theorem list.nodup.attach {α : Type u} {l : list α} :
l.nodup → l.attach.nodup

Alias of the reverse direction of list.nodup_attach.

source
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 : l.nodup) :
(list.pmap f l H).nodup
source
theorem list.nodup.filter {α : Type u} (p : α → Prop) [decidable_pred p] {l : list α} :
l.nodup → (list.filter p l).nodup
source
@[simp]
theorem list.nodup_reverse {α : Type u} {l : list α} :
l.reverse.nodup ↔ l.nodup
source
theorem list.nodup.erase_eq_filter {α : Type u} [decidable_eq α] {l : list α} (d : l.nodup) (a : α) :
l.erase a = list.filter (λ (_x : α), _x ≠ a) l
source
theorem list.nodup.erase {α : Type u} {l : list α} [decidable_eq α] (a : α) :
l.nodup → (l.erase a).nodup
source
theorem list.nodup.diff {α : Type u} {l₁ l₂ : list α} [decidable_eq α] :
l₁.nodup → (l₁.diff l₂).nodup
source
theorem list.nodup.mem_erase_iff {α : Type u} {l : list α} {a b : α} [decidable_eq α] (d : l.nodup) :
a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l
source
theorem list.nodup.not_mem_erase {α : Type u} {l : list α} {a : α} [decidable_eq α] (h : l.nodup) :
a ∉ l.erase a
source
theorem list.nodup_join {α : Type u} {L : list (list α)} :
L.join.nodup ↔ (∀ (l : list α), l ∈ L → l.nodup) ∧ list.pairwise list.disjoint L
source
theorem list.nodup_bind {α : Type u} {β : Type v} {l₁ : list α} {f : α → list β} :
(l₁.bind f).nodup ↔ (∀ (x : α), x ∈ l₁ → (f x).nodup) ∧ list.pairwise (λ (a b : α), (f a).disjoint (f b)) l₁
source
@[protected]
theorem list.nodup.product {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} (d₁ : l₁.nodup) (d₂ : l₂.nodup) :
(l₁ ×ˢ l₂).nodup
source
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
source
@[protected]
theorem list.nodup.filter_map {α : Type u} {β : Type v} {l : list α} {f : α → option β} (h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a') :
l.nodup → (list.filter_map f l).nodup
source
@[protected]
theorem list.nodup.concat {α : Type u} {l : list α} {a : α} (h : a ∉ l) (h' : l.nodup) :
(l.concat a).nodup
source
theorem list.nodup.insert {α : Type u} {l : list α} {a : α} [decidable_eq α] (h : l.nodup) :
(has_insert.insert a l).nodup
source
theorem list.nodup.union {α : Type u} {l₂ : list α} [decidable_eq α] (l₁ : list α) (h : l₂.nodup) :
(l₁ ∪ l₂).nodup
source
theorem list.nodup.inter {α : Type u} {l₁ : list α} [decidable_eq α] (l₂ : list α) :
l₁.nodup → (l₁ ∩ l₂).nodup
source
theorem list.nodup.diff_eq_filter {α : Type u} [decidable_eq α] {l₁ l₂ : list α} (hl₁ : l₁.nodup) :
l₁.diff l₂ = list.filter (λ (_x : α), _x ∉ l₂) l₁
source
theorem list.nodup.mem_diff_iff {α : Type u} {l₁ l₂ : list α} {a : α} [decidable_eq α] (hl₁ : l₁.nodup) :
a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂
source
@[protected]
theorem list.nodup.update_nth {α : Type u} {l : list α} {n : ℕ} {a : α} (hl : l.nodup) (ha : a ∉ l) :
(l.update_nth n a).nodup
source
theorem list.nodup.map_update {α : Type u} {β : Type v} [decidable_eq α] {l : list α} (hl : l.nodup) (f : α → β) (x : α) (y : β) :
list.map (function.update f x y) l = ite (x ∈ l) ((list.map f l).update_nth (list.index_of x l) y) (list.map f l)
source
theorem list.nodup.pairwise_of_forall_ne {α : Type u} {l : list α} {r : α → α → Prop} (hl : l.nodup) (h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b) :
list.pairwise r l
source
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
source
@[simp]
theorem list.nodup.pairwise_coe {α : Type u} {l : list α} {r : α → α → Prop} [is_symm α r] (hl : l.nodup) :
{a : α | a ∈ l}.pairwise r ↔ list.pairwise r l
source
theorem option.to_list_nodup {α : Type u_1} (o : option α) :
o.to_list.nodup