has_cofiltered_limits_op_of_has_filtered_colimits

English

If C has filtered colimits, then Opposite C has cofiltered limits.

Русский

Если в C существуют отфильтрованные колимиты, то в Opposite C существуют ко-филтированные пределы.

LaTeX

$$$$\\mathrm{HasCofilteredLimitsOfSize}(C^{op})\\quad\\text{given}\\quad \\mathrm{HasFilteredColimitsOfSize}(C).$$$$

Lean4

instance has_cofiltered_limits_op_of_has_filtered_colimits [HasFilteredColimitsOfSize.{v₂, u₂} C] :
    HasCofilteredLimitsOfSize.{v₂, u₂} Cᵒᵖ where HasLimitsOfShape _ _ _ := hasLimitsOfShape_op_of_hasColimitsOfShape

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