toList_getElem_eq_apply_of_lt_length

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.toList_getElem_eq_apply_of_lt_length

← MathLib Explorer

English

Variant of the previous statement for lt-length indices.

Русский

Вариант предыдущего для индексов со значением меньше длины.

LaTeX

$$Given hi, p.toList[(i)].getElem = p i$$

Lean4

theorem toList_getElem_eq_apply_of_lt_length {p : RelSeries r} {i : ℕ} (hi : i < p.length + 1) :
    p.toList[i]'(by simpa using hi) = p ⟨i, hi⟩ :=
  p.toList_getElem_eq_apply ⟨i, hi⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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