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)
:
Vector.get v i ∈ Vector.toList v
theorem
Vector.mem_iff_get
{α : Type u_1}
{n : ℕ}
(a : α)
(v : Vector α n)
:
a ∈ Vector.toList v ↔ ∃ (i : Fin n), Vector.get v i = a
theorem
Vector.mem_cons_iff
{α : Type u_1}
{n : ℕ}
(a : α)
(a' : α)
(v : Vector α n)
:
a' ∈ Vector.toList (a ::ᵥ v) ↔ a' = a ∨ a' ∈ Vector.toList v
theorem
Vector.mem_succ_iff
{α : Type u_1}
{n : ℕ}
(a : α)
(v : Vector α (n + 1))
:
a ∈ Vector.toList v ↔ a = Vector.head v ∨ a ∈ Vector.toList (Vector.tail v)
theorem
Vector.mem_cons_self
{α : Type u_1}
{n : ℕ}
(a : α)
(v : Vector α n)
:
a ∈ Vector.toList (a ::ᵥ v)
@[simp]
theorem
Vector.mem_cons_of_mem
{α : Type u_1}
{n : ℕ}
(a : α)
(a' : α)
(v : Vector α n)
(ha' : a' ∈ Vector.toList v)
:
a' ∈ Vector.toList (a ::ᵥ v)
theorem
Vector.mem_of_mem_tail
{α : Type u_1}
{n : ℕ}
(a : α)
(v : Vector α n)
(ha : a ∈ Vector.toList (Vector.tail v))
:
a ∈ Vector.toList v
theorem
Vector.mem_map_iff
{α : Type u_1}
{β : Type u_2}
{n : ℕ}
(b : β)
(v : Vector α n)
(f : α → β)
:
b ∈ Vector.toList (Vector.map f v) ↔ ∃ a ∈ Vector.toList v, f a = b
theorem
Vector.not_mem_map_zero
{α : Type u_1}
{β : Type u_2}
(b : β)
(v : Vector α 0)
(f : α → β)
:
b ∉ Vector.toList (Vector.map f v)
theorem
Vector.mem_map_succ_iff
{α : Type u_1}
{β : Type u_2}
{n : ℕ}
(b : β)
(v : Vector α (n + 1))
(f : α → β)
:
b ∈ Vector.toList (Vector.map f v) ↔ f (Vector.head v) = b ∨ ∃ a ∈ Vector.toList (Vector.tail v), f a = b