English
For a finite shape α and small I, with HasColimitsOfShape α C, the Ind.lim I preserves shape α colimits.
Русский
Для конечной формы α и малого I, имеющегося HasColimitsOfShape α C, Ind.lim I сохраняет колимиты формы α.
LaTeX
$$$[\text{Finite }\alpha] \, [\text{Small }I] \, [\text{HasColimitsOfShape }\alpha C] \Rightarrow \operatorname{PreservesColimitsOfShape}\ \alpha\ (\mathrm{Ind.lim}\ I)$$$
Lean4
instance {α : Type w} [SmallCategory α] [FinCategory α] [HasColimitsOfShape α C] {I : Type v} [SmallCategory I]
[IsFiltered I] : PreservesColimitsOfShape α (Ind.lim I : (I ⥤ C) ⥤ _) :=
inferInstanceAs (PreservesColimitsOfShape α (_ ⋙ colim))
