English
If a functor preserves filtered colimits for all sizes, then it preserves filtered colimits at the smallest size (0,0).
Русский
Если функтор сохраняет фильтрованные колимиты для всех размеров, то он сохраняет колимиты и для минимума размера (0,0).
LaTeX
$$$PreservesFilteredColimitsOfSize.{0,0} F$$$
Lean4
/-- Preserving filtered colimits at any universe implies preserving filtered colimits at universe `0`.
-/
theorem preservesSmallestFilteredColimits_of_preservesFilteredColimits (F : C ⥤ D)
[PreservesFilteredColimitsOfSize.{w', w} F] : PreservesFilteredColimitsOfSize.{0, 0} F :=
preservesFilteredColimitsOfSize_shrink F
