preservesLimits_of_op — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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