ofFn_getElem — Mathlib

English

For any l, f, the equality of ofFn (fun i => f(l[i])) with l.map f holds; i.e., ofFn (fun i : Fin l.length => f(l[(i: Nat)])) = l.map f.

Русский

Для списка l и функции f выполнено: ofFn (fun i => f(l[i])) = l.map f.

LaTeX

$$$ \\operatorname{ofFn} (\\lambda i : \\mathrm{Fin} \\ l.\\length => f(l[(i : \\mathrm{Nat})])) = l.map\\ f $$$

Lean4

@[simp]
theorem ofFn_getElem : ∀ l : List α, (ofFn (fun i : Fin l.length => l[(i : Nat)])) = l
  | [] => by rw [ofFn_zero]
  | a :: l => by
    rw [ofFn_succ]
    congr
    exact ofFn_get l

Похожие утверждения