Vectors

Lemmas about Vector α n

@[simp]

theorem Batteries.Vector.map_empty {α : Type u_1} {β : Type u_2} (f : α → β) : Batteries.Vector.map f Batteries.Vector.empty = Batteries.Vector.empty

An empty vector maps to a empty vector.

theorem Batteries.Vector.toArray_injective {α : Type u_1} {n : Nat} {v : Batteries.Vector α n} {w : Batteries.Vector α n} : v.toArray = w.toArray → v = w

theorem Batteries.Vector.eq_empty {α : Type u_1} (v : Batteries.Vector α 0) : v = Batteries.Vector.empty

A vector of length 0 is an empty vector.

theorem Batteries.Vector.ext_iff {α : Type u_1} {n : Nat} {a : Batteries.Vector α n} {b : Batteries.Vector α n} : a = b ↔ ∀ (i : Nat) (x : i < n), a[i] = b[i]

theorem Batteries.Vector.ext {α : Type u_1} {n : Nat} {a : Batteries.Vector α n} {b : Batteries.Vector α n} (h : ∀ (i : Nat) (x : i < n), a[i] = b[i]) : a = b

Vector.ext is an extensionality theorem. Vectors a and b are equal to each other if their elements are equal for each valid index.