English
For a finite shape α and a filtered index I, the functor Ind.lim I preserves limits of shape α.
Русский
Для конечной формы α и фильтрованного индекса I транспортер Ind.lim I сохраняет пределы формы α.
LaTeX
$$$[\text{Finite }\alpha] \, [\text{IsFiltered }I] \Rightarrow \operatorname{PreservesLimitsOfShape}\ \alpha\ (\mathrm{Ind.lim}\ I)$$$
Lean4
instance {α : Type w} [SmallCategory α] [FinCategory α] [HasLimitsOfShape α C] {I : Type v} [SmallCategory I]
[IsFiltered I] : PreservesLimitsOfShape α (Ind.lim I : (I ⥤ C) ⥤ _) :=
haveI : PreservesLimitsOfShape α (Ind.lim I ⋙ Ind.inclusion C) :=
preservesLimitsOfShape_of_natIso Ind.limCompInclusion.symm
preservesLimitsOfShape_of_reflects_of_preserves _ (Ind.inclusion C)
