evaluationPreservesLimits — Mathlib

English

Assuming limits exist in C, the evaluation functor ev_k: K ⥤ C → C preserves limits.

Русский

При условии существования пределов в C, функция оценки ev_k сохраняет пределы.

LaTeX

$$$\operatorname{evaluation}_{k}: K \to C$ preserves limits$$

Lean4

instance evaluationPreservesLimits [HasLimits C] (k : K) : PreservesLimits ((evaluation K C).obj k) where
  preservesLimitsOfShape {_} _𝒥 := inferInstance

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