toFinsupp_apply_fin

Mathlib.Data.List.ToFinsupp

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

English

For finite index n (as a Fin), the value matches the corresponding list element.

Русский

Для конечного индекса n (как Fin), значение совпадает с соответствующим элементом списка.

LaTeX

$$$$ l.toFinsupp n = l[n], \\quad n: \\text{Fin } |l|. $$$$

Lean4

theorem toFinsupp_apply_fin (n : Fin l.length) : l.toFinsupp n = l[n] :=
  getD_eq_getElem _ _ n.isLt

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

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

Разделы

Аффилиация

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