preservesLimitsOfSize_leftOp — Mathlib

English

If F.unop: C ⥤ D preserves colimits, then F: C^{op} ⥤ D^{op} preserves limits.

Русский

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

LaTeX

$$$(F: C^{op} \to D) [PreservesColimitsOfSize{w,w'}(F.unop)] \Rightarrow (F: C \to D^{op}) [PreservesLimitsOfSize{w,w'}(F)].$$$

Lean4

/-- If `F : C ⥤ Dᵒᵖ` preserves colimits, then `F.leftOp : Cᵒᵖ ⥤ D` preserves limits. -/
theorem preservesLimitsOfSize_leftOp (F : C ⥤ Dᵒᵖ) [PreservesColimitsOfSize.{w, w'} F] :
    PreservesLimitsOfSize.{w, w'} F.leftOp where preservesLimitsOfShape {_} _ := preservesLimitsOfShape_leftOp _ _

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