hasColimits_of_hasLimits_op — Mathlib

English

If HasLimitsOfSize in C^op holds, then HasColimitsOfSize in C holds.

Русский

Если в C^op существуют пределы заданного размера, то в C существуют колимиты заданного размера.

LaTeX

$$$[HasLimitsOfSize \\; (\\mathrm{Opposite}\, C)] \\Rightarrow [HasColimitsOfSize \\; C]$$$

Lean4

theorem hasColimits_of_hasLimits_op [HasLimitsOfSize.{v₂, u₂} Cᵒᵖ] : HasColimitsOfSize.{v₂, u₂} C :=
  { has_colimits_of_shape := fun _ _ => hasColimitsOfShape_of_hasLimitsOfShape_op }

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