append_reverseAux — Mathlib

English

The reverse map from G.Walk u v to itself is surjective: every walk has a reverse that is a valid walk in the graph.

Русский

Обратное отображение путей в графе сюръективно: каждый путь имеет обратный путь на графе.

LaTeX

$$$$\text{For all } u,v,\text{ reverse}: G.Walk\ u\ v \to _\text{is surjective}.$$$$

Lean4

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

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