preservesColimitsOfShape_leftOp — Mathlib

English

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

Русский

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

LaTeX

$$$\\operatorname{PreservesColimitsOfShape} J F^{\\mathrm{leftOp}}$$$

Lean4

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

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