hasLimitsOfShape

Mathlib.CategoryTheory.Limits.Comma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Arrow.hasLimitsOfShape

English

If T has limits of shape J, then Arrow T has limits of shape J.

Русский

Если в категории T существуют пределы формы J, то в категории стрелок Arrow T тоже существуют пределы формы J.

LaTeX

$$HasLimitsOfShape J T \\Rightarrow HasLimitsOfShape J (Arrow T)$$

Lean4

instance hasLimitsOfShape [HasLimitsOfShape J T] : HasLimitsOfShape J (Arrow T) where

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

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

Разделы

Аффилиация

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