preservesLimitsOfShape_of_leftOp — Mathlib

English

If F: C → D^{op} preserves colimits of shape J^{op}, then F.leftOp: C^{op} ⥤ D preserves limits of shape J.

Русский

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

LaTeX

$$$(F: C \to D^{op}) [PreservesColimitsOfShape(J^{op}, F.leftOp)] \Rightarrow (F.leftOp: C^{op} \to D) [PreservesLimitsOfShape(J, F)].$$$

Lean4

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

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