preservesFiniteLimits_of_rightOp — Mathlib

English

Let F: C^{op} → D. If the rightOp of F preserves finite colimits, then F preserves finite limits.

Русский

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

LaTeX

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

Lean4

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

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