mapReverseComp — Mathlib

English

The reverse map is compatible with the composition of prefuntors: (φ ⋙q ψ).map (reverse e) = reverse ((φ ⋙q ψ).map e).

Русский

Обратное отображение совместимо с композицией префункторов: (φ ⋙q ψ).map(reverse e) = reverse((φ ⋙q ψ).map e).

LaTeX

$$$ (\\varphi \\;⋙q\\; \\psi).map(\\mathrm{reverse}~e) = \\mathrm{reverse}((\\varphi \\;⋙q\\; \\psi).map~e) $$$

Lean4

instance _root_.Prefunctor.mapReverseComp (φ : U ⥤q V) (ψ : V ⥤q W) [φ.MapReverse] [ψ.MapReverse] : (φ ⋙q ψ).MapReverse
    where map_reverse' e := by simp only [Prefunctor.comp_map, Prefunctor.MapReverse.map_reverse']

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