hasIterationOfShape

Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

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

English

The statement asserts the existence of a HasIterationOfShape κ.ord.toType C under the given hypotheses.

Русский

Утверждается существование HasIterationOfShape κ.ord.toType для C при данных предпосылках.

LaTeX

$$HasIterationOfShape κ.ord.toType C$$

Lean4

theorem hasIterationOfShape : HasIterationOfShape κ.ord.toType C :=
  IsCardinalForSmallObjectArgument.hasIterationOfShape I

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

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

Разделы

Аффилиация

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