instAB5IndOfHasFiniteLimits

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization

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

English

If C has finite limits, then Ind(C) has AB5 with respect to size, i.e., AB5 of size for Ind.

Русский

Если C имеет конечные пределы, то Ind(C) имеет AB5 по размеру (AB5 для Ind).

LaTeX

$$$\mathrm{AB5}(\mathrm{Ind}\,C)$$$

Lean4

instance [HasFiniteLimits C] : AB5 (Ind C) where ofShape _ _ _ := inferInstance

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

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

Разделы

Аффилиация

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