last_reverse

Mathlib.Order.RelSeries

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

English

The last element of the reverse of p is the head of p.

Русский

Последний элемент обращения p совпадает с головой p.

LaTeX

$$$ (p.reverse).last = p.head $$$

Lean4

@[simp]
theorem last_reverse (p : RelSeries r) : p.reverse.last = p.head := by simp [RelSeries.last, RelSeries.head]

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

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

Разделы

Аффилиация

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