instPreservesColimitsOfShapeEvalOfHasColimitsOfShape

English

For each n, eval C c n preserves colimits of shape J, given that J-colimits exist in C.

Русский

Для каждого n функция оценки сохраняет колимиты формы J при условии существования колимитов формы J в C.

LaTeX

$$$ \forall n, \mathrm{PreservesColimitsOfShape}(J, \mathrm{eval}_{n}). $$$

Lean4

noncomputable instance [HasColimitsOfShape J C] (n : ι) : PreservesColimitsOfShape J (eval C c n) :=
  ⟨inferInstance⟩

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