preservesLimits_unop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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