last_take

Mathlib.Order.RelSeries

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

English

The last element of the prefix taking p at i is the i-th element of p.

Русский

Последний элемент префикса p на i равен i-му элементу p.

LaTeX

$$$$ (\\mathrm{take}(p,i)).\\text{last} = p(i). $$$$

Lean4

@[simp]
theorem last_take (p : RelSeries r) (i : Fin (p.length + 1)) : (p.take i).last = p i := by simp [take, last, Fin.last]

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

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

Разделы

Аффилиация

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