Theorems about `List.ofFn` #

def List.ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) :

ofFn f with f : fin n → α returns the list whose ith element is f i

ofFn f = [f 0, f 1, ... , f (n - 1)]

Equations

@[simp]

theorem List.length_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) :

(ofFn f).length = n

@[simp]

theorem List.getElem_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length) :

(ofFn f)[i] = f ⟨i, ⋯⟩

@[simp]

theorem List.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 List.ofFn_zero {α : Type u_1} (f : Fin 0 → α) :

ofFn f = []

ofFn on an empty domain is the empty list.

@[simp]

theorem List.ofFn_succ {α : Type u_1} {n : Nat} (f : Fin (n + 1) → α) :

ofFn f = f 0 :: ofFn fun (i : Fin n) => f i.succ

@[simp]

theorem List.ofFn_eq_nil_iff {n : Nat} {α : Type u_1} {f : Fin n → α} :

ofFn f = [] ↔ n = 0

theorem List.head_ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (h : ofFn f ≠ []) :

(ofFn f).head h = f ⟨0, ⋯⟩

theorem List.getLast_ofFn {α : Type u_1} {n : Nat} (f : Fin n → α) (h : ofFn f ≠ []) :

(ofFn f).getLast h = f ⟨n - 1, ⋯⟩

Documentation