mathlib documentation

theorem list.forall_mem_ne {α : Type u} {a : α} {l : list α} :

theorem list.nodup_nil {α : Type u} :

theorem list.nodup_cons {α : Type u} {a : α} {l : list α} :

theorem list.rel_nodup {α : Type u} {β : Type v} {r : α → β → Prop} (hr : relator.bi_unique r) :

theorem list.nodup_cons_of_nodup {α : Type u} {a : α} {l : list α} (m : a ∉ l) (n : l.nodup) :

theorem list.nodup_singleton {α : Type u} (a : α) :

theorem list.nodup_of_nodup_cons {α : Type u} {a : α} {l : list α} (h : (a :: l).nodup) :

theorem list.not_mem_of_nodup_cons {α : Type u} {a : α} {l : list α} (h : (a :: l).nodup) :

theorem list.not_nodup_cons_of_mem {α : Type u} {a : α} {l : list α} (a_1 : a ∈ l) :

theorem list.nodup_of_sublist {α : Type u} {l₁ l₂ : list α} (a : l₁ <+ l₂) (a_1 : l₂.nodup) :

theorem list.not_nodup_pair {α : Type u} (a : α) :

theorem list.nodup_iff_sublist {α : Type u} {l : list α} :

theorem list.nodup_iff_nth_le_inj {α : Type u} {l : list α} :

theorem list.nth_le_index_of {α : Type u} [decidable_eq α] {l : list α} (H : l.nodup) (n : ℕ) (h : n < l.length) :

theorem list.nodup_iff_count_le_one {α : Type u} [decidable_eq α] {l : list α} :

theorem list.nodup_repeat {α : Type u} (a : α) {n : ℕ} :

theorem list.count_eq_one_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} (d : l.nodup) (h : a ∈ l) :

theorem list.nodup_of_nodup_append_left {α : Type u} {l₁ l₂ : list α} (a : (l₁ ++ l₂).nodup) :

theorem list.nodup_of_nodup_append_right {α : Type u} {l₁ l₂ : list α} (a : (l₁ ++ l₂).nodup) :

theorem list.nodup_append {α : Type u} {l₁ l₂ : list α} :

theorem list.disjoint_of_nodup_append {α : Type u} {l₁ l₂ : list α} (d : (l₁ ++ l₂).nodup) :

theorem list.nodup_append_of_nodup {α : Type u} {l₁ l₂ : list α} (d₁ : l₁.nodup) (d₂ : l₂.nodup) (dj : l₁.disjoint l₂) :

theorem list.nodup_append_comm {α : Type u} {l₁ l₂ : list α} :

theorem list.nodup_middle {α : Type u} {a : α} {l₁ l₂ : list α} :

theorem list.nodup_of_nodup_map {α : Type u} {β : Type v} (f : α → β) {l : list α} (a : (list.map f l).nodup) :

theorem list.nodup_map_on {α : Type u} {β : Type v} {f : α → β} {l : list α} (H : ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ l → f x = f y → x = y) (d : l.nodup) :

theorem list.nodup_map {α : Type u} {β : Type v} {f : α → β} {l : list α} (hf : function.injective f) (a : l.nodup) :

theorem list.nodup_map_iff {α : Type u} {β : Type v} {f : α → β} {l : list α} (hf : function.injective f) :

theorem list.nodup_attach {α : Type u} {l : list α} :

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) :

theorem list.nodup_filter {α : Type u} (p : α → Prop) [decidable_pred p] {l : list α} (a : l.nodup) :

theorem list.nodup_reverse {α : Type u} {l : list α} :

theorem list.nodup_erase_eq_filter {α : Type u} [decidable_eq α] (a : α) {l : list α} (d : l.nodup) :

theorem list.nodup_erase_of_nodup {α : Type u} [decidable_eq α] (a : α) {l : list α} (a_1 : l.nodup) :

theorem list.nodup_diff {α : Type u} [decidable_eq α] {l₁ l₂ : list α} (h : l₁.nodup) :

theorem list.mem_erase_iff_of_nodup {α : Type u} [decidable_eq α] {a b : α} {l : list α} (d : l.nodup) :

theorem list.mem_erase_of_nodup {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : l.nodup) :

theorem list.nodup_join {α : Type u} {L : list (list α)} :

theorem list.nodup_bind {α : Type u} {β : Type v} {l₁ : list α} {f : α → list β} :

theorem list.nodup_product {α : Type u} {β : Type v} {l₁ : list α} {l₂ : list β} (d₁ : l₁.nodup) (d₂ : l₂.nodup) :

theorem list.nodup_sigma {α : Type u} {σ : α → Type u_1} {l₁ : list α} {l₂ : Π (a : α), list (σ a)} (d₁ : l₁.nodup) (d₂ : ∀ (a : α), (l₂ a).nodup) :

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') (a : l.nodup) :

theorem list.nodup_concat {α : Type u} {a : α} {l : list α} (h : a ∉ l) (h' : l.nodup) :

theorem list.nodup_insert {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : l.nodup) :

theorem list.nodup_union {α : Type u} [decidable_eq α] (l₁ : list α) {l₂ : list α} (h : l₂.nodup) :

theorem list.nodup_inter_of_nodup {α : Type u} [decidable_eq α] {l₁ : list α} (l₂ : list α) (a : l₁.nodup) :

theorem list.nodup_sublists {α : Type u} {l : list α} :

theorem list.nodup_sublists' {α : Type u} {l : list α} :

theorem list.nodup_sublists_len {α : Type u_1} (n : ℕ) {l : list α} (nd : l.nodup) :

theorem list.diff_eq_filter_of_nodup {α : Type u} [decidable_eq α] {l₁ l₂ : list α} (hl₁ : l₁.nodup) :

theorem list.mem_diff_iff_of_nodup {α : Type u} [decidable_eq α] {l₁ l₂ : list α} (hl₁ : l₁.nodup) {a : α} :

theorem list.nodup_update_nth {α : Type u} {l : list α} {n : ℕ} {a : α} (hl : l.nodup) (ha : a ∉ l) :

theorem option.to_list_nodup {α : Type u_1} (o : option α) :