append_assoc — Mathlib

English

Walk concatenation is associative: p.append(q.append(r)) = (p.append q).append(r) for walks p, q, r.

Русский

Сложение путей ассоциативно: p.append(q.append(r)) = (p.append q).append(r).

LaTeX

$$$$\forall {u,v,w,x} (p : G.Walk u v)(q : G.Walk v w)(r : G.Walk w x),\ p.append(q.append(r)) = (p.append q).append(r).$$$$

Lean4

theorem append_assoc {u v w x : V} (p : G.Walk u v) (q : G.Walk v w) (r : G.Walk w x) :
    p.append (q.append r) = (p.append q).append r := by
  induction p with
  | nil => rw [nil_append, nil_append]
  | cons h p' ih => rw [cons_append, cons_append, cons_append, ih]

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