preservesLimits_rightOp — Mathlib

English

If F: Cᵒᵖ ⥤ D preserves colimits, then F.rightOp: C ⥤ Dᵒᵖ preserves limits.

Русский

Если F: C^{op} ⥤ D сохраняет колимиты, то F.rightOp: C ⥤ D^{op} сохраняет пределы.

LaTeX

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

Lean4

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

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