preservesColimits_rightOp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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