reflectsSmallestCofilteredLimits_of_reflectsCofilteredLimits

English

If F reflects cofiltered limits for some size, then it reflects the smallest case (0,0).

Русский

Если F отражает когильтрованные пределы для некоторого размера, то отражает наименьший случай (0,0).

LaTeX

$$$\text{ReflectsCofilteredLimitsOfSize}(F;0,0)$$$

Lean4

/-- Reflecting cofiltered limits at any universe implies reflecting cofiltered limits at universe `0`.
-/
theorem reflectsSmallestCofilteredLimits_of_reflectsCofilteredLimits (F : C ⥤ D)
    [ReflectsCofilteredLimitsOfSize.{w', w} F] : ReflectsCofilteredLimitsOfSize.{0, 0} F :=
  reflectsCofilteredLimitsOfSize_shrink F

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