last_snoc

Mathlib.Order.RelSeries

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

English

The last element of a snoc is the newly added element: (p.snoc newLast rel).last = newLast.

Русский

Последний элемент snoc есть вновь добавленный элемент: (p.snoc newLast rel).last = newLast.

LaTeX

$$$ (p.\text{snoc } newLast\ rel).\text{last} = newLast $$$

Lean4

@[simp]
theorem last_snoc (p : RelSeries r) (newLast : α) (rel : p.last ~[r] newLast) : (p.snoc newLast rel).last = newLast :=
  last_append _ _ _

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

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

Разделы

Аффилиация

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