English
The shrink lemma: from a larger universes assumption, one can deduce a smaller-universe reflection of colimits. Specifically, if ReflectsColimitsOfSize^{max w w2, max w' w2'} F holds, then ReflectsColimitsOfSize^{w, w'} F holds.
Русский
Лемма сжатия: из условия отражения колимит в больших вселенных следует отражение в меньших вселенных. Единичное выражение: если ReflectsColimitsOfSize^{max w w2, max w' w2'} F, то ReflectsColimitsOfSize^{w, w'} F.
LaTeX
$$$\\forall w,w'\\; (\\text{UnivLE}^{\\max w w2,\\max w' w2'}F) \\Rightarrow (ReflectsColimitsOfSize^{w,w'}F)$.$$
Lean4
/-- `reflectsColimitsOfSize_shrink.{w w'} F` tries to obtain `reflectsColimitsOfSize.{w w'} F`
from some other `reflectsColimitsOfSize F`.
-/
theorem reflectsColimitsOfSize_shrink (F : C ⥤ D) [ReflectsColimitsOfSize.{max w w₂, max w' w₂'} F] :
ReflectsColimitsOfSize.{w, w'} F :=
reflectsColimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F
