preservesLimits_of_rightOp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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