getI_eq_getElem

Mathlib.Data.List.GetD

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

English

For any list l and index n, getI n equals the nth element of l when it exists.

Русский

Для списка l и индекса n getI n равен n-му элементу списка, если он существует.

LaTeX

$$$$ \\forall l\\; \\forall n:\\; \\text{instLTNat.lt} \\ n \\ l.length \\Rightarrow \\ \\text{getI}\\ n = l[n] $$$$

Lean4

theorem getI_eq_getElem {n : ℕ} (hn : n < l.length) : l.getI n = l[n] :=
  getD_eq_getElem l default hn

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

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

Разделы

Аффилиация

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