hasCofilteredLimitsOfSize_of_hasLimitsOfSize

English

If a category C has all limits of a given size (w', w), then it has all cofiltered limits of that size.

Русский

Если категория C обладает пределами заданного размера (w', w), то у неё существуют кофильтрованные пределы того же размера.

LaTeX

$$$HasLimitsOfSize^{w',w}(C) \Rightarrow HasCofilteredLimitsOfSize^{w',w}(C)$$$

Lean4

instance (priority := 100) hasCofilteredLimitsOfSize_of_hasLimitsOfSize [HasLimitsOfSize.{w', w} C] :
    HasCofilteredLimitsOfSize.{w', w} C where HasLimitsOfShape _ _ _ := inferInstance

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