getElem_range'_1

Mathlib.Data.List.Range

URI: https://scilib.ai/kg/mathlib#List.getElem_range'_1

English

If i is less than the length of range' n m, then the i-th element equals n + i.

Русский

Если i меньше длины range' n m, тогда i-й элемент равен n + i.

LaTeX

$$$\text{getElem}_{getElemRange'}(n,m,i,H) = n + i$$$

Lean4

theorem getElem_range'_1 {n m} (i) (H : i < (range' n m).length) : (range' n m)[i] = n + i := by simp

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

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

Разделы

Аффилиация

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