mapComposableArrows — Mathlib

English

Reiterates that the object component matches the given obj under the constructed instance.

Русский

Повторное утверждение равенства компонента объектов для построенного примера.

LaTeX

$$$(mkOfObjOfMapSucc obj mapSucc).obj i = obj i$$$

Lean4

/-- The functor `ComposableArrows C n ⥤ ComposableArrows D n` obtained by postcomposition
with a functor `C ⥤ D`. -/
@[simps!]
def mapComposableArrows : ComposableArrows C n ⥤ ComposableArrows D n :=
  (whiskeringRight _ _ _).obj G

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