mathlib documentation

data.vector.mem

Theorems about membership of elements in vectors #

This file contains theorems for membership in a v.to_list 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.nth_mem {α : Type u_1} {n : } (i : fin n) (v : vector α n) :
theorem vector.mem_iff_nth {α : Type u_1} {n : } (a : α) (v : vector α n) :
a v.to_list ∃ (i : fin n), v.nth i = a
theorem vector.not_mem_nil {α : Type u_1} (a : α) :
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' (a ::ᵥ v).to_list a' = a a' v.to_list
theorem vector.mem_succ_iff {α : Type u_1} {n : } (a : α) (v : vector α (n + 1)) :
theorem vector.mem_cons_self {α : Type u_1} {n : } (a : α) (v : vector α n) :
a (a ::ᵥ v).to_list
@[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' v.to_list) :
a' (a ::ᵥ v).to_list
theorem vector.mem_of_mem_tail {α : Type u_1} {n : } (a : α) (v : vector α n) (ha : a v.tail.to_list) :
theorem vector.mem_map_iff {α : Type u_1} {β : Type u_2} {n : } (b : β) (v : vector α n) (f : α → β) :
b (vector.map f v).to_list ∃ (a : α), a v.to_list 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.map f v).to_list f v.head = b ∃ (a : α), a v.tail.to_list f a = b