locallySmall

Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.locallySmall

English

There is a HasIterationOfShape κ.ord.toType in a given category C for the morphism property I.

Русский

Существует HasIterationOfShape κ.ord.toType в данной категории C для свойства морфизмов I.

LaTeX

$$HasIterationOfShape κ.ord.toType C$$

Lean4

theorem locallySmall : LocallySmall.{w} C :=
  IsCardinalForSmallObjectArgument.locallySmall I κ

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

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

Разделы

Аффилиация

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