getLast_toList

Mathlib.Order.RelSeries

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

← MathLib Explorer

English

For any RelSeries p, the last element of its toList equals p.last.

Русский

Для любой последовательности RelSeries p, последний элемент её списка toList равен p.last.

LaTeX

$$$ \\operatorname{getLast}(p) = p.last $$$

Lean4

@[simp]
theorem getLast_toList (p : RelSeries r) : p.toList.getLast (by simp [toList]) = p.last := by
  simp [last, ← toList_getElem_eq_apply, List.getLast_eq_getElem]

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

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

Разделы

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

Аффилиация

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