preservesSmallestLimits_of_preservesLimits

English

Preserving limits at any universe level implies preserving limits in universe 0.

Русский

Сохранение пределов на любом уровне вселенных следует из сохранения пределов вселенной 0.

LaTeX

$$$ \\mathrm{PreservesLimitsOfSize}^{(v_3,u_3)}(F) \\Rightarrow \\mathrm{PreservesLimitsOfSize}^{(0,0)}(F).$$$

Lean4

/-- Preserving limits at any universe level implies preserving limits in universe `0`. -/
theorem preservesSmallestLimits_of_preservesLimits (F : C ⥤ D) [PreservesLimitsOfSize.{v₃, u₃} F] :
    PreservesLimitsOfSize.{0, 0} F :=
  preservesLimitsOfSize_shrink F

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