hasLimit_of_hasColimit_rightOp — Mathlib

English

If HasColimit F, then HasLimit F.rightOp.

Русский

Если у F существует колимит, то существует предел F.rightOp.

LaTeX

$$$$ \\operatorname{HasColimit}(F) \\Rightarrow \\operatorname{HasLimit}(F^{\\mathrm{rightOp}}) $$$$

Lean4

theorem hasLimit_of_hasColimit_rightOp (F : Jᵒᵖ ⥤ C) [HasColimit F.rightOp] : HasLimit F :=
  HasLimit.mk
    { cone := coneOfCoconeRightOp (colimit.cocone F.rightOp)
      isLimit := isLimitConeOfCoconeRightOp _ (colimit.isColimit _) }

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