head_ofFn

Mathlib.Data.Vector.Basic

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

English

The head of the vector obtained from a function f on Fin(n+1) is f(0).

Русский

Голова вектора, полученного из функции f на Fin(n+1), равна f(0).

LaTeX

$$$\\forall {n}\\; (f:\\mathrm{Fin}(n.succ)\\to \\alpha),\\; \\mathrm{head}(\\mathrm{ofFn}(f)) = f(0)$$$

Lean4

@[simp]
theorem head_ofFn {n : ℕ} (f : Fin n.succ → α) : head (ofFn f) = f 0 := by rw [← get_zero, get_ofFn]

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

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

Разделы

Аффилиация

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