hasFilteredColimitsOfSize_of_hasColimitsOfSize

English

If C has colimits of size w' and w, then has filtered colimits of the same size: HasFilteredColimitsOfSize C.

Русский

Если C имеет колимиты размера w' и w, то имеет фильтрованные колимиты того же размера: HasFilteredColimitsOfSize C.

LaTeX

$$$ HasFilteredColimitsOfSize\\ C $$$

Lean4

instance (priority := 100) hasFilteredColimitsOfSize_of_hasColimitsOfSize [HasColimitsOfSize.{w', w} C] :
    HasFilteredColimitsOfSize.{w', w} C where HasColimitsOfShape _ _ _ := inferInstance

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