comp_preservesLimits — Mathlib

English

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

Русский

Если F и 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_preservesLimits [PreservesLimitsOfSize.{w', w} F] [PreservesLimitsOfSize.{w', w} G] :
    PreservesLimitsOfSize.{w', w} (F ⋙ G) where

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