hasColimitsOfSizeShrink — Mathlib

English

If a category C has colimits of size (max(v1, v2), max(u1, u2)), then it also has colimits of size (v1, u1).

Русский

Если категория C имеет колимиты размером (max(v1, v2), max(u1, u2)), то она также имеет колимиты размером (v1, u1).

LaTeX

$$$ [\mathrm{HasColimitsOfSize}(\max(v_1,v_2), \max(u_1,u_2); C)] \Rightarrow [\mathrm{HasColimitsOfSize}(v_1,u_1; C)]. $$$

Lean4

/-- `hasColimitsOfSizeShrink.{v u} C` tries to obtain `HasColimitsOfSize.{v u} C`
from some other `HasColimitsOfSize C`.
-/
theorem hasColimitsOfSizeShrink [HasColimitsOfSize.{max v₁ v₂, max u₁ u₂} C] : HasColimitsOfSize.{v₁, u₁} C :=
  hasColimitsOfSizeOfUnivLE.{max v₁ v₂, max u₁ u₂} C

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