preservesColimitsOfSize_shrink — Mathlib

English

Preservation of colimits of shape is stable under shrinking the universe levels.

Русский

Сохранение колимитов по форме устойчиво к сжатию уровней вселенной.

LaTeX

$$$ (F)\\; [PreservesColimitsOfSize F] \\Rightarrow \\mathrm{PreservesColimitsOfSize}^{(w,w')} F. $$$

Lean4

/-- `PreservesColimitsOfSize_shrink.{w w'} F` tries to obtain `PreservesColimitsOfSize.{w w'} F`
from some other `PreservesColimitsOfSize F`.
-/
theorem preservesColimitsOfSize_shrink (F : C ⥤ D) [PreservesColimitsOfSize.{max w w₂, max w' w₂'} F] :
    PreservesColimitsOfSize.{w, w'} F :=
  preservesColimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

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