English
If C has cofiltered limits of size (w₂', w₂) and the universe bounds relate as UnivLE.{w,w₂}, UnivLE.{w',w₂'}, then HasCofilteredLimitsOfSize.{w', w} C holds.
Русский
Если C имеет кофильтрованные пределы размера (w₂', w₂) и соотношения уровней вселенных удовлетворяют UnivLE, то существует HasCofilteredLimitsOfSize.{w', w} C.
LaTeX
$$$[UnivLE^{w,w₂}] [UnivLE^{w',w₂'}] [HasCofilteredLimitsOfSize^{w₂',w₂} C] \Rightarrow HasCofilteredLimitsOfSize^{w',w} C$$$
Lean4
theorem hasCofilteredLimitsOfSize_of_univLE [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}]
[HasCofilteredLimitsOfSize.{w₂', w₂} C] : HasCofilteredLimitsOfSize.{w', w} C where
HasLimitsOfShape
J :=
haveI :=
IsCofiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂'} J).trans <| Shrink.equivalence.{w₂} (ShrinkHoms.{w} J))
hasLimitsOfShape_of_equivalence
((ShrinkHoms.equivalence.{w₂'} J).trans <| Shrink.equivalence.{w₂} (ShrinkHoms.{w} J)).symm
