getLast_ofFn_succ

Mathlib.Data.List.OfFn

URI: https://scilib.ai/kg/mathlib#List.getLast_ofFn_succ

← MathLib Explorer

English

If f: Fin (n+1) → α, the last element of List.ofFn f equals f(Fin.last n).

Русский

Если f: Fin(n+1) → α, то последний элемент List.ofFn f равен f(Fin.last n).

LaTeX

$$$ (\\operatorname{List.ofFn} f).getLast = f(\\mathrm{Fin.last} \\, n) $$$

Lean4

theorem getLast_ofFn_succ {n : ℕ} (f : Fin n.succ → α) :
    (ofFn f).getLast (mt ofFn_eq_nil_iff.1 (Nat.succ_ne_zero _)) = f (Fin.last _) :=
  getLast_ofFn _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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