append_assoc — Mathlib

English

Two-step associativity: (p ⧺ q) ⧺ w equals p ⧺ (q ⧺ w) for all compatible p, q, w.

Русский

Два шага ассоциативности: (p ⧺ q) ⧺ w равно p ⧺ (q ⧺ w) для всех согласованных тройных p, q, w.

LaTeX

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

Lean4

theorem append_assoc (p q w : RelSeries r) (hpq : p.last ~[r] q.head) (hqw : q.last ~[r] w.head) :
    (p.append q hpq).append w (by simpa) = p.append (q.append w hqw) (by simpa) :=
  by
  ext
  · simp only [append_length, Nat.add_left_inj]
    cutsat
  · simp [append, Fin.append_assoc]

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