mapBifunctorLeftUnitor_hasMap — Mathlib

English

A variant stating the existence of HasMap for the left unitor applied to mapBifunctor on X.

Русский

Вариант утверждает существование HasMap для левого унитора, применённого к mapBifunctor на X.

LaTeX

$$$$mapBifunctorLeftUnitor_hasMap : HasMap ( (mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y p.$$$$

Lean4

theorem mapBifunctorLeftUnitor_hasMap : HasMap (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y) p :=
  CofanMapObjFun.hasMap _ _ _ (mapBifunctorLeftUnitorCofanIsColimit F X e p hp Y)

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