preservesLimitsOfShape_leftOp — Mathlib

English

If F preserves limits of K.leftOp, then F.leftOp preserves colimits of K.

Русский

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

LaTeX

$$$\\operatorname{PreservesColimit} K F^{\\mathrm{leftOp}}$$$

Lean4

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

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