reverse_append — Mathlib

English

For any two walks p: u → v and q: v → w, the reverse of their concatenation equals the concatenation of their reverses in reverse order: Reverse(p ∘ q) = Reverse(q) ∘ Reverse(p).

Русский

Для двух путей p: u→v и q: v→w обратная последовательность их конкатенации равна конкатенации их обратных в противоположном порядке: Reverse(p ∘ q) = Reverse(q) ∘ Reverse(p).

LaTeX

$$$\mathrm{Reverse}(p \append q) = \mathrm{Reverse}(q) \append \mathrm{Reverse}(p)$$$

Lean4

@[simp]
theorem reverse_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) :
    (p.append q).reverse = q.reverse.append p.reverse := by simp [reverse]

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