comp_reflectsLimitsOfShape — Mathlib

English

Another instance showing that ReflectsLimitsOfShape is preserved under composition of functors.

Русский

Еще один пример того, как ReflectsLimitsOfShape сохраняется при композиции функторов.

LaTeX

$$$ [ReflectsLimitsOfShape J F] [ReflectsLimitsOfShape J G] \\Rightarrow \\text{ReflectsLimitsOfShape } J (F \\cdot G). $$$

Lean4

instance comp_reflectsLimitsOfShape [ReflectsLimitsOfShape J F] [ReflectsLimitsOfShape J G] :
    ReflectsLimitsOfShape J (F ⋙ G) where

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