comp_preservesColimits — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance comp_preservesColimits [PreservesColimitsOfSize.{w', w} F] [PreservesColimitsOfSize.{w', w} G] :
    PreservesColimitsOfSize.{w', w} (F ⋙ G) where

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