English
If a functor F preserves cofiltered limits of some size, then it preserves the (0,0) cofiltered limits, i.e., all finite cofiltered limits.
Русский
Если функтор F сохраняет пределы когильтрованных диаграмм заданного размера, то он сохраняет пределы когильтрованных диаграмм размера (0,0), то есть все конечные когильтрованные пределы.
LaTeX
$$$PreservesCofilteredLimitsOfSize(F;0,0)$$$
Lean4
/-- Preserving cofiltered limits at any universe implies preserving cofiltered limits at universe `0`.
-/
theorem preservesSmallestCofilteredLimits_of_preservesCofilteredLimits (F : C ⥤ D)
[PreservesCofilteredLimitsOfSize.{w', w} F] : PreservesCofilteredLimitsOfSize.{0, 0} F :=
preservesCofilteredLimitsOfSize_shrink F
