hasFiniteColimits_of_hasCountableColimits

English

Let C be a category. If C has all countable colimits, then C has all finite colimits.

Русский

Пусть C — категория. Если в C существуют все счётные колимиты, то в C существуют все конечные колимиты.

LaTeX

$$$ \\operatorname{HasCountableColimits}(\\mathcal{C}) \\Rightarrow \\operatorname{HasFiniteColimits}(\\mathcal{C}) $$$

Lean4

instance (priority := 100) hasFiniteColimits_of_hasCountableColimits [HasCountableColimits C] : HasFiniteColimits C
    where out J := HasCountableColimits.out J

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