@[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 α} :
l.nodup → a ∈ l → list.count a l = 1
theorem
list.nodup_map
{α : Type u}
{β : Type v}
{f : α → β}
{l : list α} :
function.injective f → l.nodup → (list.map f l).nodup
theorem
list.nodup_map_iff
{α : Type u}
{β : Type v}
{f : α → β}
{l : list α} :
function.injective f → ((list.map f l).nodup ↔ l.nodup)
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 α} :
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_insert
{α : Type u}
[decidable_eq α]
{a : α}
{l : list α} :
l.nodup → (has_insert.insert a l).nodup
theorem
list.nodup_sublists_len
{α : Type u_1}
(n : ℕ)
{l : list α} :
l.nodup → (list.sublists_len n l).nodup
theorem
list.diff_eq_filter_of_nodup
{α : Type u}
[decidable_eq α]
{l₁ l₂ : list α} :
l₁.nodup → l₁.diff l₂ = list.filter (λ (_x : α), _x ∉ l₂) l₁
theorem
list.nodup_update_nth
{α : Type u}
{l : list α}
{n : ℕ}
{a : α} :
l.nodup → a ∉ l → (l.update_nth n a).nodup