ofMapReverse — Mathlib

English

If V is a quiver with reverse, there is a MapReverse instance for Push.of σ, defined using the reverse of σ.

Русский

Если имеется квир V с обратным, существует инстанс MapReverse для Push.of σ, заданный через обратное отображение σ.

LaTeX

$$$ (Push.of\\, \\sigma).MapReverse $$$

Lean4

instance ofMapReverse [h : HasInvolutiveReverse V] : (Push.of σ).MapReverse :=
  ⟨by simp [of_reverse]⟩

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