Lists with no duplicates #
list.nodup is defined in data/list/defs. In this file we prove various properties of this
predicate.
@[protected]
theorem
list.pairwise.nodup
{α : Type u}
{l : list α}
{r : α → α → Prop}
[is_irrefl α r]
(h : list.pairwise r l) :
l.nodup
@[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
theorem
list.nodup_iff_count_le_one
{α : Type u}
[decidable_eq α]
{l : list α} :
l.nodup ↔ ∀ (a : α), list.count a l ≤ 1
@[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
theorem
list.nodup_map
{α : Type u}
{β : Type v}
{f : α → β}
{l : list α}
(hf : function.injective f) :
theorem
list.nodup_map_iff
{α : Type u}
{β : Type v}
{f : α → β}
{l : list α}
(hf : function.injective f) :
theorem
list.nodup_filter
{α : Type u}
(p : α → Prop)
[decidable_pred p]
{l : list α} :
l.nodup → (list.filter p l).nodup
theorem
list.nodup_erase_eq_filter
{α : Type u}
[decidable_eq α]
(a : α)
{l : list α}
(d : l.nodup) :
l.erase a = list.filter (λ (_x : α), _x ≠ a) l
theorem
list.nodup_join
{α : Type u}
{L : list (list α)} :
L.join.nodup ↔ (∀ (l : list α), l ∈ L → l.nodup) ∧ list.pairwise list.disjoint L
theorem
list.nodup_filter_map
{α : Type u}
{β : Type v}
{f : α → option β}
{l : list α}
(H : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a') :
l.nodup → (list.filter_map f l).nodup
theorem
list.nodup_sublists_len
{α : Type u_1}
(n : ℕ)
{l : list α}
(nd : l.nodup) :
(list.sublists_len n l).nodup
theorem
list.diff_eq_filter_of_nodup
{α : Type u}
[decidable_eq α]
{l₁ l₂ : list α}
(hl₁ : l₁.nodup) :
l₁.diff l₂ = list.filter (λ (_x : α), _x ∉ l₂) l₁
theorem
list.nodup_update_nth
{α : Type u}
{l : list α}
{n : ℕ}
{a : α}
(hl : l.nodup)
(ha : a ∉ l) :
(l.update_nth n a).nodup
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)
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
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