hasColimitsOfShape_of_essentiallySmall

English

If J is essentially small and C has colimits of size, then HasColimitsOfShape J C.

Русский

Если J существенно мал, и C имеет колимиты размера, то HasColimitsOfShape J C.

LaTeX

$$$ HasColimitsOfShape\\ J\\ C $$$

Lean4

theorem hasColimitsOfShape_of_essentiallySmall [EssentiallySmall.{w₁} J] [HasColimitsOfSize.{w₁, w₁} C] :
    HasColimitsOfShape J C :=
  hasColimitsOfShape_of_equivalence <| Equivalence.symm <| equivSmallModel.{w₁} J

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