AB5StarOfSize_shrink — Mathlib

English

Let C be a category with cofiltered limits. If C satisfies AB5Star for large sizes, then it also satisfies AB5Star for smaller sizes.

Русский

Пусть C — категория с кофильтрованными пределами. Если C удовлетворяет AB5Star для больших размеров, то она удовлетворяет AB5Star и для меньших размеров.

LaTeX

$$$\\operatorname{HasCofilteredLimitsOfSize}^{(\\text{large})}(C) \\land \\operatorname{AB5StarOfSize}^{(\\text{large})}(C) \\Rightarrow \\operatorname{HasCofilteredLimitsOfSize}^{(w,w')}(C) \\land \\operatorname{AB5StarOfSize}^{(w,w')}(C)$$$

Lean4

theorem AB5StarOfSize_shrink [HasCofilteredLimitsOfSize.{max w w₂, max w' w₂'} C]
    [AB5StarOfSize.{max w w₂, max w' w₂'} C] :
    haveI : HasCofilteredLimitsOfSize.{w, w'} C := hasCofilteredLimitsOfSize_shrink
    AB5StarOfSize.{w, w'} C :=
  AB5StarOfSize_of_univLE C

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