reverse_concat — Mathlib

English

The reverse of a concatenation with an edge equals a simple cons with reversed edge and reversed path: (p.concat h).reverse = cons (G.symm h) p.reverse.

Русский

Обратное к конкатенации с ребром равно простому cons с обращённым ребром и обращённым путём: (p.concat h).reverse = cons (G.symm h) p.reverse.

LaTeX

$$$$\forall {p,h},\ (p.concat h).reverse = \text{cons}(G.symm(h), p.reverse).$$$$

Lean4

@[simp]
theorem reverse_concat {u v w : V} (p : G.Walk u v) (h : G.Adj v w) :
    (p.concat h).reverse = cons (G.symm h) p.reverse := by simp [concat_eq_append]

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