mapActionPreservesLimitsOfShapeOfPreserves

English

If F preserves limits of shape J and V has limits of shape J, then F.mapAction G preserves limits of shape J.

Русский

Если F сохраняет пределы формы J и V имеет пределы формы J, то F.mapAction G сохраняет пределы формы J.

LaTeX

$$$\\operatorname{PreservesLimitsOfShape}(J, F.mapAction\\,G)$$$

Lean4

/-- `F.mapAction : Action V G ⥤ Action W G` preserves limits of some shape `J` if
`V` has limits of shape `J` and `F` preserves limits of shape `J`. -/
instance mapActionPreservesLimitsOfShapeOfPreserves [PreservesLimitsOfShape J F] [HasLimitsOfShape J V] :
    PreservesLimitsOfShape J (F.mapAction G) where

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