last_append — Mathlib

English

The append operation is associative: (p ⧺ q) ⧺ w equals p ⧺ (q ⧺ w) up to the obvious identifications when the linking edges match.

Русский

Операция конкатенации ассоциативна: (p ⧺ q) ⧺ w эквивалентна p ⧺ (q ⧺ w) при совпадающих соединительных ребрах.

LaTeX

$$$ (p \\append q) \\append w = p \\append (q \\append w) $$$

Lean4

@[simp]
theorem last_append (p q : RelSeries r) (connect : p.last ~[r] q.head) : (p.append q connect).last = q.last :=
  by
  delta last
  convert append_apply_right p q connect (Fin.last _)
  ext1
  dsimp
  omega

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