reflectsSmallestLimits_of_reflectsLimits

English

Reflecting limits at any universe implies reflecting limits at universe 0.

Русский

Отражение пределов в любой вселенной влечет отражение пределов вселенной 0.

LaTeX

$$$\\forall F\\;[\\mathrm{ReflectsLimitsOfSize}\\,(F)] \\Rightarrow [\\mathrm{ReflectsLimitsOfSize}\\,0\\,0\\ (F)]$$$

Lean4

/-- Reflecting limits at any universe implies reflecting limits at universe `0`. -/
theorem reflectsSmallestLimits_of_reflectsLimits (F : C ⥤ D) [ReflectsLimitsOfSize.{v₃, u₃} F] :
    ReflectsLimitsOfSize.{0, 0} F :=
  reflectsLimitsOfSize_shrink F

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