preservesLimits_of_unop — Mathlib

English

If F.unop preserves colimits, then F preserves limits.

Русский

Если F.unop сохраняет колимиты, то F сохраняет пределы.

LaTeX

$$$\operatorname{PreservesColimits}(F^{\mathrm{unop}}) \Rightarrow \operatorname{PreservesLimits}(F)$$$

Lean4

/-- If `F.unop : C ⥤ D` preserves colimits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits. -/
theorem preservesLimits_of_unop (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesColimits F.unop] : PreservesLimits F where
  preservesLimitsOfShape {_} _ := preservesLimitsOfShape_of_unop _ _

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