reverse_reverse — Mathlib

English

For any quiver V with HasInvolutiveReverse, reversing an arrow twice yields the original arrow.

Русский

Для кивера V с свойством HasInvolutiveReverse обратное стрелке применённое дважды возвращает исходную стрелку.

LaTeX

$$$ \\forall {a b : V}, \\mathrm{reverse}(\\mathrm{reverse}(f)) = f $$$

Lean4

@[simp]
theorem reverse_reverse [h : HasInvolutiveReverse V] {a b : V} (f : a ⟶ b) : reverse (reverse f) = f := by apply h.inv'

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