comp_preservesColimitsOfShape — Mathlib

English

If F and G preserve colimits of size J, then F ⋙ G preserves colimits of size J.

Русский

Если F и G сохраняют колимиты размера J, тогда F ⋙ G сохраняет колимиты размера J.

LaTeX

$$$$\mathrm{PreservesColimitsOfSize}(J,F) \land \mathrm{PreservesColimitsOfSize}(J,G) \Rightarrow \mathrm{PreservesColimitsOfSize}(J,F\circ G).$$$$

Lean4

instance comp_preservesColimitsOfShape [PreservesColimitsOfShape J F] [PreservesColimitsOfShape J G] :
    PreservesColimitsOfShape J (F ⋙ G) where

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