hasLimit_leftOp_of_hasColimit — Mathlib

English

If HasColimit F, then HasLimit F.leftOp.

Русский

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

LaTeX

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

Lean4

instance hasLimit_leftOp_of_hasColimit (F : J ⥤ Cᵒᵖ) [HasColimit F] : HasLimit F.leftOp :=
  HasLimit.mk
    { cone := coneLeftOpOfCocone (colimit.cocone F)
      isLimit := isLimitConeLeftOpOfCocone _ (colimit.isColimit _) }

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