Theorems about membership of elements in vectors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

@[simp]

theorem vector.nth_mem {α : Type u_1} {n : ℕ} (i : fin n) (v : vector α n) :

v.nth i ∈ v.to_list

source

theorem vector.mem_iff_nth {α : Type u_1} {n : ℕ} (a : α) (v : vector α n) :

a ∈ v.to_list ↔ ∃ (i : fin n), v.nth i = a

source

theorem vector.not_mem_nil {α : Type u_1} (a : α) :

a ∉ vector.nil.to_list

source

theorem vector.not_mem_zero {α : Type u_1} (a : α) (v : vector α 0) :

a ∉ v.to_list

source

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

source

theorem vector.mem_succ_iff {α : Type u_1} {n : ℕ} (a : α) (v : vector α (n + 1)) :

a ∈ v.to_list ↔ a = v.head ∨ a ∈ v.tail.to_list

source

theorem vector.mem_cons_self {α : Type u_1} {n : ℕ} (a : α) (v : vector α n) :

a ∈ (a ::ᵥ v).to_list

source

@[simp]

theorem vector.head_mem {α : Type u_1} {n : ℕ} (v : vector α (n + 1)) :

v.head ∈ v.to_list

source

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

source

theorem vector.mem_of_mem_tail {α : Type u_1} {n : ℕ} (a : α) (v : vector α n) (ha : a ∈ v.tail.to_list) :

a ∈ v.to_list

source

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

source

theorem vector.not_mem_map_zero {α : Type u_1} {β : Type u_2} (b : β) (v : vector α 0) (f : α → β) :

b ∉ (vector.map f v).to_list

source

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