reflectsFilteredColimitsOfSize_shrink

English

Shrinking the universe preserves the reflection property for filtered colimits.

Русский

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

LaTeX

$$$reflectsFilteredColimitsOfSize\\_shrink(F)$$$

Lean4

/-- `ReflectsFilteredColimitsOfSize_shrink.{w, w'} F` tries to obtain
`ReflectsFilteredColimitsOfSize.{w, w'} F` from some other `ReflectsFilteredColimitsOfSize F`.
-/
theorem reflectsFilteredColimitsOfSize_shrink (F : C ⥤ D) [ReflectsFilteredColimitsOfSize.{max w w₂, max w' w₂'} F] :
    ReflectsFilteredColimitsOfSize.{w, w'} F :=
  reflectsFilteredColimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

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