getElem?_length

Mathlib.Data.List.Basic

URI: https://scilib.ai/kg/mathlib#List.getElem?_length

English

For any list l, the optional get element at position length l is none.

Русский

Для любого списка l опциональный доступ к элементу на позиции length l дает none.

LaTeX

$$$ l[l.length]? = \text{none} $$$

Lean4

theorem getElem?_length (l : List α) : l[l.length]? = none :=
  getElem?_eq_none le_rfl

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

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

Разделы

Аффилиация

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