hasLimit_of_hasColimit_unop — Mathlib

English

If HasColimit F, then HasLimit F.unop.

Русский

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

LaTeX

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

Lean4

theorem hasLimit_of_hasColimit_unop (F : Jᵒᵖ ⥤ Cᵒᵖ) [HasColimit F.unop] : HasLimit F :=
  HasLimit.mk
    { cone := coneOfCoconeUnop (colimit.cocone F.unop)
      isLimit := isLimitConeOfCoconeUnop _ (colimit.isColimit _) }

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