reverseAux_append — Mathlib

English

For any p and q, the reverseAux of concatenating p and q equals the reverse of q appended to the reverse of p.

Русский

Для любых путей p и q, reverseAux(p,q) равен reverse(q) append reverse(p).

LaTeX

$$$$\forall {p,q},\ p.reverseAux q = p.reverse.append q.$$$$

Lean4

@[simp]
protected theorem reverseAux_append {u v w x : V} (p : G.Walk u v) (q : G.Walk u w) (r : G.Walk w x) :
    (p.reverseAux q).append r = p.reverseAux (q.append r) := by
  induction p with
  | nil => rfl
  | cons h _ ih => simp [ih (cons (G.symm h) q)]

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