preservesFiniteLimits_unop — Mathlib

English

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

Русский

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

LaTeX

$$$\operatorname{PreservesFiniteLimits}(F) \Rightarrow \operatorname{PreservesFiniteColimits}(F^{\mathrm{unop}})$$$

Lean4

/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite colimits, then `F.unop : C ⥤ D` preserves finite
limits. -/
theorem preservesFiniteLimits_unop (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesFiniteColimits F] : PreservesFiniteLimits F.unop where
  preservesFiniteLimits J _ _ := preservesLimitsOfShape_unop J F

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