comp_hasColimit — Mathlib

English

IsColimitExtendCoconeEquiv t gives an equivalence between colimit-ness of extendCocone.obj t and t.

Русский

IsColimitExtendCoconeEquiv t задаёт эквивалентность между колимитностью extendCocone.obj t и t.

LaTeX

$$$$ \text{IsColimit}(\operatorname{extendCocone.obj} t) \simeq \text{IsColimit}(t). $$$$

Lean4

instance (priority := 100) comp_hasColimit [HasColimit G] : HasColimit (F ⋙ G) :=
  HasColimit.mk (colimitCoconeComp F (getColimitCocone G))

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