preservesLimitsOfShape_rightOp — Mathlib

English

If F preserves colimits of shape Jᵒᵖ, then F.op preserves colimits of J.

Русский

Если F сохраняет колимиты формы Jᵒᵖ, то F.op сохраняет колимиты формы J.

LaTeX

$$$\\operatorname{preservesColimitsOfShape} J F^{\\mathrm{op}}$$$

Lean4

/-- If `F : Cᵒᵖ ⥤ D` preserves colimits of shape `Jᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` preserves limits
of shape `J`. -/
theorem preservesLimitsOfShape_rightOp (F : Cᵒᵖ ⥤ D) [PreservesColimitsOfShape Jᵒᵖ F] :
    PreservesLimitsOfShape J F.rightOp where preservesLimit {K} := preservesLimit_rightOp K F

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