ofFn_get — Mathlib

English

For any list l, the list built from the function i ↦ l[i] equals l itself; i.e., ofFn (fun i : Fin l.length => l[(i: Nat)]) = l.

Русский

Для любого списка l список, построенный по функции i ↦ l[i], равен самому l; то есть ofFn (fun i : Fin l.length => l[(i: Nat)]) = l.

LaTeX

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

Lean4

@[simp]
theorem ofFn_get : ∀ l : List α, (ofFn (get l)) = l
  | [] => by rw [ofFn_zero]
  | a :: l => by
    rw [ofFn_succ]
    congr
    exact ofFn_get l

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