hasColimitsOfShape — Mathlib

English

If A has limits of all sizes and G preserves limits of those sizes, then CostructuredArrow G X has colimits of those sizes.

Русский

Если A имеет пределы всех размеров, и G сохраняет пределы этих размеров, то CostructuredArrow G X имеет колимиты этих размеров.

LaTeX

$$$\\operatorname{HasColimitsOfSize}(\\mathrm{CostructuredArrow}\\, G\\, X)$$$

Lean4

instance hasColimitsOfShape [HasColimitsOfShape J A] [PreservesColimitsOfShape J G] :
    HasColimitsOfShape J (CostructuredArrow G X) where

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