concat_append — Mathlib

English

The end of a concatenation and subsequent append satisfy: p.concat h appended to q equals p appended with cons h q. More precisely, p.concat h .append q = p.append (cons h q).

Русский

Завершение конкатенации и последующее добавление удовлетворяют: p.concat h .append q = p.append (cons h q).

LaTeX

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

Lean4

theorem concat_append {u v w x : V} (p : G.Walk u v) (h : G.Adj v w) (q : G.Walk w x) :
    (p.concat h).append q = p.append (cons h q) := by rw [concat_eq_append, ← append_assoc, cons_nil_append]

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