hasCountableColimits_of_hasColimits

Mathlib.CategoryTheory.Limits.Shapes.Countable

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.hasCountableColimits_of_hasColimits

English

If C has all colimits, then C has all countable colimits.

Русский

Если в C существуют все колимиты, то в C существуют все счётные колимиты.

LaTeX

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

Lean4

instance (priority := 100) hasCountableColimits_of_hasColimits [HasColimits C] : HasCountableColimits C where
  out := inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru