toFinsupp_apply_lt

Mathlib.Data.List.ToFinsupp

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

English

If n < length(l), then the value at n equals the nth element of l.

Русский

Если n меньше длины l, то значение на позиции n равно n-му элементу списка.

LaTeX

$$$$ \\text{If } n < |l|, \\; l\\toFinsupp(n) = l[n]. $$$$

Lean4

theorem toFinsupp_apply_lt (hn : n < l.length) : l.toFinsupp n = l[n] :=
  getD_eq_getElem _ _ hn

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

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

Разделы

Аффилиация

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