hasCofilteredLimitsOfSize_shrink — Mathlib

English

Shrinking the universe level preserves cofiltered limits: if HasCofilteredLimitsOfSize at the broad level, then HasCofilteredLimitsOfSize at the smaller level.

Русский

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

LaTeX

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

Lean4

theorem hasCofilteredLimitsOfSize_shrink [HasCofilteredLimitsOfSize.{max w' w₂', max w w₂} C] :
    HasCofilteredLimitsOfSize.{w', w} C :=
  hasCofilteredLimitsOfSize_of_univLE.{w', w, max w' w₂', max w w₂}

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