mvfunctor — Mathlib

English

Cofix F is equipped with a functor structure whose map is given by Cofix.map. This provides a functorial action on Cofix F compatible with Morphisms.

Русский

Cofix F наделён структурой функторов; отображение определяется Cofix.map и задаёт функторное действие на Cofix F.

LaTeX

$$$\\mathrm{mvfunctor}\\;\\text{Cofix F} \\;:\\; \\text{MvFunctor}\\,(\\mathrm{Cofix}\\,F)$ and $\\mathrm{map} = \\mathrm{Cofix.map}$.$$

Lean4

instance mvfunctor : MvFunctor (Cofix F) where map := @Cofix.map _ _ _

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