reverse_comp — Mathlib

English

In a quiver with reverse, reversing a concatenation of paths satisfies: (p ⋅ q).reverse = q.reverse ⋅ p.reverse.

Русский

В кивере с обратным порядком стрелок выполнение: (p ⋅ q).reverse = q.reverse ⋅ p.reverse.

LaTeX

$$$ (p \\cdot q)^{\\mathrm{reverse}} = q^{\\mathrm{reverse}} \\cdot p^{\\mathrm{reverse}} $$$

Lean4

@[simp]
theorem reverse_comp [HasReverse V] {a b c : V} (p : Path a b) (q : Path b c) :
    (p.comp q).reverse = q.reverse.comp p.reverse := by
  induction q with
  | nil => simp
  | cons _ _ h => simp [h]

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