preservesFilteredColimitsOfSize_shrink

English

Shrinking the universe size yields the same preservation property for filtered colimits.

Русский

Сужение размера вселенной сохраняет сохранение фильтрованных колимитов.

LaTeX

$$$preservesFilteredColimitsOfSize\\_shrink(F)$$$

Lean4

/-- `PreservesFilteredColimitsOfSize_shrink.{w, w'} F` tries to obtain
`PreservesFilteredColimitsOfSize.{w, w'} F` from some other `PreservesFilteredColimitsOfSize F`.
-/
theorem preservesFilteredColimitsOfSize_shrink (F : C ⥤ D) [PreservesFilteredColimitsOfSize.{max w w₂, max w' w₂'} F] :
    PreservesFilteredColimitsOfSize.{w, w'} F :=
  preservesFilteredColimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

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