preservesLimitsOfSize_of_preserves

English

If F preserves limits of a given size and V has limits of that size, then F.mapAction G preserves limits of that size.

Русский

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

LaTeX

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

Lean4

/-- `F.mapAction : Action V G ⥤ Action W G` preserves limits of some size if
`V` has limits of that size and `F` preserves limits of that size. -/
instance preservesLimitsOfSize_of_preserves [PreservesLimitsOfSize.{w₂, w₁} F] [HasLimitsOfSize.{w₂, w₁} V] :
    PreservesLimitsOfSize.{w₂, w₁} (F.mapAction G) where

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