append_concat — Mathlib

English

A nontrivial concatenation p.concat h (where h is an edge from the end of p) can be written as a concatenation q.concat h' with a new starting vertex and edge h'. There exist x, q, h' with p.concat h = q.concat h'.

Русский

Непреступное объединение p.concat h можно записать как q.concat h' с новым началом; существуют x, q, h' такие, что p.concat h = q.concat h'.

LaTeX

$$$$\forall {u,v,w} (p : G.Walk u v)(h : G.Adj v w),\ \exists x\, \exists q : G.Walk u x\, \exists h' : G.Adj x w,\ p.concat h = q.concat h'.$$$$

Lean4

theorem append_concat {u v w x : V} (p : G.Walk u v) (q : G.Walk v w) (h : G.Adj w x) :
    p.append (q.concat h) = (p.append q).concat h :=
  append_assoc _ _ _

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