hasLimitsOfShape_of_essentiallySmall

English

If J is essentially small and C has limits of size, then C has all limits of shape J, i.e., HasLimitsOfShape J C.

Русский

Если J является существенно малым, и C имеет пределы размера, то в C существуют пределы формы J, т.е. HasLimitsOfShape J C.

LaTeX

$$$ HasLimitsOfShape\\ J\\ C $$$

Lean4

theorem hasLimitsOfShape_of_essentiallySmall [EssentiallySmall.{w₁} J] [HasLimitsOfSize.{w₁, w₁} C] :
    HasLimitsOfShape J C :=
  hasLimitsOfShape_of_equivalence <| Equivalence.symm <| equivSmallModel.{w₁} J

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