reverse_cons — Mathlib

English

The reverse of a cons with an adjacent edge is equal to the concatenation of the reverse of the original and a final edge; more precisely, (cons h p).reverse = p.reverse.append (cons (G.symm h) nil).

Русский

Обратное к конструктору cons с сопряжённым ребром равно конкатенации обратного исходного пути и завершающего ребра; то есть (cons h p).reverse = p.reverse.append (cons (G.symm h) nil).

LaTeX

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

Lean4

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

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