get_ofFn — Mathlib

English

Let f: Fin n → α. Then the i-th element of the list representation of f equals f evaluated at the corresponding index; i.e., (ofFn f) i = f(Fin.cast i).

Русский

Пусть f: Fin n → α. Тогда i-й элемент списка, соответствующего f, равен f, применённому к соответствующему индексу; т.е. (ofFn f) i = f(Fin.cast i).

LaTeX

$$$ (\\operatorname{get} (\\operatorname{ofFn}(f)) \\, i) = f(\\operatorname{Fin.cast} i) $$$

Lean4

theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f (Fin.cast (by simp) i) := by simp; congr

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