instHasColimitsOfSizeUnder

Mathlib.CategoryTheory.WithTerminal.Cone

URI: https://scilib.ai/kg/mathlib#instHasColimitsOfSizeUnder

English

For any C with HasColimitsOfSize and X, Under X has HasColimitsOfSize.

Русский

Пусть C имеет колимиты заданного размера; тогда Under X имеет колимиты заданного размера.

LaTeX

$$HasColimitsOfSize (Under X)$$

Lean4

instance (X : C) [HasColimitsOfSize.{w, w'} C] : HasColimitsOfSize.{w, w'} (Under X) where

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

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

Разделы

Аффилиация

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