# Documentation

Mathlib.Data.Vector.Mem

# 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 Vector.get_mem {α : Type u_1} {n : } (i : Fin n) (v : Vector α n) :
theorem Vector.mem_iff_get {α : Type u_1} {n : } (a : α) (v : Vector α n) :
i, = a
theorem Vector.not_mem_nil {α : Type u_1} (a : α) :
¬a Vector.toList Vector.nil
theorem Vector.not_mem_zero {α : Type u_1} (a : α) (v : Vector α 0) :
theorem Vector.mem_cons_iff {α : Type u_1} {n : } (a : α) (a' : α) (v : Vector α n) :
a' Vector.toList (a ::ᵥ v) a' = a a'
theorem Vector.mem_succ_iff {α : Type u_1} {n : } (a : α) (v : Vector α (n + 1)) :
a =
theorem Vector.mem_cons_self {α : Type u_1} {n : } (a : α) (v : Vector α n) :
@[simp]
theorem Vector.head_mem {α : Type u_1} {n : } (v : Vector α (n + 1)) :
theorem Vector.mem_cons_of_mem {α : Type u_1} {n : } (a : α) (a' : α) (v : Vector α n) (ha' : a' ) :
theorem Vector.mem_of_mem_tail {α : Type u_1} {n : } (a : α) (v : Vector α n) (ha : ) :
theorem Vector.mem_map_iff {α : Type u_1} {β : Type u_2} {n : } (b : β) (v : Vector α n) (f : αβ) :
b Vector.toList () a, f a = b
theorem Vector.not_mem_map_zero {α : Type u_1} {β : Type u_2} (b : β) (v : Vector α 0) (f : αβ) :
theorem Vector.mem_map_succ_iff {α : Type u_1} {β : Type u_2} {n : } (b : β) (v : Vector α (n + 1)) (f : αβ) :
b Vector.toList () f () = b a, f a = b