instHasCardinalFilteredColimitsOfHasColimitsOfSize

English

If C has colimits of a given size, then C has κ-filtered colimits for that κ.

Русский

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

LaTeX

$$$[HasColimitsOfSize C] \Rightarrow [HasCardinalFilteredColimits C \kappa]$$$

Lean4

instance [HasColimitsOfSize.{w, w} C] : HasCardinalFilteredColimits.{w} C κ where

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