get_ofFn

Mathlib.Data.Vector.Basic

URI: https://scilib.ai/kg/mathlib#List.Vector.get_ofFn

English

For any function f defined on Fin n, the i-th element of the vector ofFn f is f i.

Русский

Для любой функции f на Fin n, i-й элемент вектора fromFn f равен f i.

LaTeX

$$$\forall n\; f:\mathrm{Fin}\,n\to\alpha,\; \mathrm{get}(\mathrm{ofFn}\ f)\ i = f\ i$$$

Lean4

@[simp]
theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f i := by simp [get_eq_get_toList]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru