hasColimit_rightOp_of_hasLimit — Mathlib

English

If C has colimits of the shape Opposite J, then C has limits of shape J.

Русский

Если в C существуют колимиты формы Opposite J, то в C существуют пределы формы J.

LaTeX

$$$$\\mathrm{HasLimitsOfShape}(J, C)$$$$

Lean4

instance hasColimit_rightOp_of_hasLimit (F : Jᵒᵖ ⥤ C) [HasLimit F] : HasColimit F.rightOp :=
  HasColimit.mk
    { cocone := coconeRightOpOfCone (limit.cone F)
      isColimit := isColimitCoconeRightOpOfCone _ (limit.isLimit _) }

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