map_reverse — Mathlib

English

A Prefunctor preserves reversal: map (reverse e) equals reverse (map e).

Русский

Префунктор сохраняет разворот: отображение(reverse e) равно развороту отображения e.

LaTeX

$$$ \\phi.map(\\mathrm{reverse}~e) = \\mathrm{reverse}(\\phi.map~e) $$$

Lean4

@[simp]
theorem _root_.Prefunctor.map_reverse (φ : U ⥤q V) [φ.MapReverse] {u v : U} (e : u ⟶ v) :
    φ.map (reverse e) = reverse (φ.map e) :=
  Prefunctor.MapReverse.map_reverse' e

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