last_cons — Mathlib

English

The last element of the cons-constructed series equals the last element of the original series.

Русский

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

LaTeX

$$$ (p.cons newHead rel).last = p.last $$$

Lean4

@[simp]
theorem last_cons (p : RelSeries r) (newHead : α) (rel : newHead ~[r] p.head) : (p.cons newHead rel).last = p.last :=
  by
  delta cons
  rw [last_append]

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