instLawfulMvFunctorObj — Mathlib

English

There is a LawfulMvFunctor instance for P.Obj, with id_map and comp_map given by the corresponding theorems.

Русский

Существует экземпляр LawfulMvFunctor для P.Obj, где id_map и comp_map задаются соответствующими теоремами.

LaTeX

$$$$ \\text{Lawful mv-functor structure on } P.Obj \\text{ with } id\\_map, comp\\_map. $$$$

Lean4

instance : LawfulMvFunctor.{u} P.Obj where
  id_map := @id_map _ P
  comp_map := @comp_map _ P

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