preservesLimitsOfSize_unop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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