hasFilteredColimitsOfSize_shrink — Mathlib

English

Shrinking universes preserves filtered colimits: HasFilteredColimitsOfSize at broad level implies HasFilteredColimitsOfSize at smaller level.

Русский

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

LaTeX

$$$[HasFilteredColimitsOfSize^{\max w' w_2', \max w w_2} C] \Rightarrow HasFilteredColimitsOfSize^{w',w} C$$$

Lean4

theorem hasFilteredColimitsOfSize_shrink [HasFilteredColimitsOfSize.{max w' w₂', max w w₂} C] :
    HasFilteredColimitsOfSize.{w', w} C :=
  hasFilteredColimitsOfSize_of_univLE.{w', w, max w' w₂', max w w₂}

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