preservesColimits_unop — Mathlib

English

If F preserves limits, then F.unop preserves colimits.

Русский

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

LaTeX

$$$\operatorname{PreservesLimits}(F) \Rightarrow \operatorname{PreservesColimits}(F^{\mathrm{unop}})$$$

Lean4

/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits, then `F.unop : C ⥤ D` preserves colimits. -/
theorem preservesColimits_unop (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesLimits F] : PreservesColimits F.unop where
  preservesColimitsOfShape {_} _ := preservesColimitsOfShape_unop _ _

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