last_smash — Mathlib

English

Let p and q be finite relation series with p.last = q.head. Then the last element of smash(p,q,h) is the last element of q.

Русский

Пусть p и q — конечные реляционные ряды с условием p.last = q.head. Тогда последний элемент smash(p,q,h) равен последнему элементу q.

LaTeX

$$$$ (\\text{smash}(p,q,h)).\\text{last} = q.\\text{last}. $$$$

Lean4

@[simp]
theorem last_smash {p q : RelSeries r} (h : p.last = q.head) : (smash p q h).last = q.last :=
  by
  dsimp only [smash, last]
  rw [← Fin.natAdd_last, Fin.addCases_right]

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