comp_preservesLimitsOfShape — Mathlib

English

If F and G preserve limits of shape J, then their composition F ⋙ G preserves limits of shape J.

Русский

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

LaTeX

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

Lean4

instance comp_preservesLimitsOfShape [PreservesLimitsOfShape J F] [PreservesLimitsOfShape J G] :
    PreservesLimitsOfShape J (F ⋙ G) where

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