preservesLimitsOfSize_shrink — Mathlib

English

If a functor F preserves limits of a large enough size, then it also preserves limits of any smaller size.

Русский

Если функтор F сохраняет пределы для достаточно больших размеров, то он сохраняет пределы и для любых меньших размеров.

LaTeX

$$$ \\mathrm{PreservesLimitsOfSize}^{(\\max(w,w_2),\\max(w',w_2'))}(F) \\Rightarrow \\mathrm{PreservesLimitsOfSize}^{(w,w')}(F).$$$

Lean4

/-- `PreservesLimitsOfSize_shrink.{w w'} F` tries to obtain `PreservesLimitsOfSize.{w w'} F`
from some other `PreservesLimitsOfSize F`.
-/
theorem preservesLimitsOfSize_shrink (F : C ⥤ D) [PreservesLimitsOfSize.{max w w₂, max w' w₂'} F] :
    PreservesLimitsOfSize.{w, w'} F :=
  preservesLimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

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