hasLimitsOfShape_of_initiallySmall

English

If J is initially small, then HasLimitsOfShape J C holds for C with limits of appropriate size.

Русский

Если J первоначально мал, то HasLimitsOfShape J C имеет пределы нужного размера в C.

LaTeX

$$$[\\text{InitiallySmall } J] \\Rightarrow \\text{HasLimitsOfShape } J\\; C$$$

Lean4

theorem hasLimitsOfShape_of_initiallySmall (J : Type u) [Category.{v} J] [InitiallySmall.{w} J] (C : Type u₁)
    [Category.{v₁} C] [HasLimitsOfSize.{w, w} C] : HasLimitsOfShape J C :=
  Initial.hasLimitsOfShape_of_initial (fromInitialModel J)

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