evaluation_preservesLimitsOfShape

English

For a functor F: J ⥤ K ⥤ C, for each k ∈ K the evaluation component ev_k preserves limits of shape J.

Русский

Для функторa F: J ⥤ K ⥤ C, для каждого k ∈ K компонент ev_k сохраняет пределы формы J.

LaTeX

$$$\forall k,\ PreservesLimitsOfShape(J, (\mathrm{ev}_k))$$$

Lean4

instance evaluation_preservesLimitsOfShape [HasLimitsOfShape J C] (k : K) :
    PreservesLimitsOfShape J ((evaluation K C).obj k) where preservesLimit := inferInstance

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