preservesFiniteColimits_of_unop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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