Theorems about Vector.ofFn

@[simp]

theorem Vector.getElem_ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (i : Nat) (h : i < n) : (ofFn f)[i] = f ⟨i, h⟩

theorem Vector.getElem?_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) : (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

@[simp]

theorem Vector.mem_ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ ∃ (i : Fin n), f i = a

theorem Vector.back_ofFn {α : Type u_1} {n : Nat} [NeZero n] (f : Fin n → α) : (ofFn f).back = f ⟨n - 1, ⋯⟩