Theorems about membership of elements in vectors

This file contains theorems for membership in a v.toList for a vector v. Having the length available in the type allows some of the lemmas to be simpler and more general than the original version for lists. In particular we can avoid some assumptions about types being Inhabited, and make more general statements about head and tail.

@[simp]

theorem List.Vector.get_mem {α : Type u_1} {n : ℕ} (i : Fin n) (v : Vector α n) : v.get i ∈ v.toList

theorem List.Vector.mem_iff_get {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n) : a ∈ v.toList ↔ ∃ (i : Fin n), v.get i = a

theorem List.Vector.notMem_nil {α : Type u_1} (a : α) : a ∉ nil.toList

@[deprecated List.Vector.notMem_nil (since := "2025-05-23")]

theorem List.Vector.not_mem_nil {α : Type u_1} (a : α) : a ∉ nil.toList

Alias of List.Vector.notMem_nil.

theorem List.Vector.notMem_zero {α : Type u_1} (a : α) (v : Vector α 0) : a ∉ v.toList

@[deprecated List.Vector.notMem_zero (since := "2025-05-23")]

theorem List.Vector.not_mem_zero {α : Type u_1} (a : α) (v : Vector α 0) : a ∉ v.toList

Alias of List.Vector.notMem_zero.

theorem List.Vector.mem_cons_iff {α : Type u_1} {n : ℕ} (a a' : α) (v : Vector α n) : a' ∈ (a ::ᵥ v).toList ↔ a' = a ∨ a' ∈ v.toList

theorem List.Vector.mem_succ_iff {α : Type u_1} {n : ℕ} (a : α) (v : Vector α (n + 1)) : a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList

theorem List.Vector.mem_cons_self {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n) : a ∈ (a ::ᵥ v).toList

@[simp]

theorem List.Vector.head_mem {α : Type u_1} {n : ℕ} (v : Vector α (n + 1)) : v.head ∈ v.toList

theorem List.Vector.mem_cons_of_mem {α : Type u_1} {n : ℕ} (a a' : α) (v : Vector α n) (ha' : a' ∈ v.toList) : a' ∈ (a ::ᵥ v).toList

theorem List.Vector.mem_of_mem_tail {α : Type u_1} {n : ℕ} (a : α) (v : Vector α n) (ha : a ∈ v.tail.toList) : a ∈ v.toList

theorem List.Vector.mem_map_iff {α : Type u_1} {β : Type u_2} {n : ℕ} (b : β) (v : Vector α n) (f : α → β) : b ∈ (map f v).toList ↔ ∃ a ∈ v.toList, f a = b

theorem List.Vector.notMem_map_zero {α : Type u_1} {β : Type u_2} (b : β) (v : Vector α 0) (f : α → β) : b ∉ (map f v).toList

@[deprecated List.Vector.notMem_map_zero (since := "2025-05-23")]

theorem List.Vector.not_mem_map_zero {α : Type u_1} {β : Type u_2} (b : β) (v : Vector α 0) (f : α → β) : b ∉ (map f v).toList

Alias of List.Vector.notMem_map_zero.

theorem List.Vector.mem_map_succ_iff {α : Type u_1} {β : Type u_2} {n : ℕ} (b : β) (v : Vector α (n + 1)) (f : α → β) : b ∈ (map f v).toList ↔ f v.head = b ∨ ∃ a ∈ v.tail.toList, f a = b