hasLimitsOfShape — Mathlib

English

If J is a shape category and HasLimitsOfShape J C holds, then HasLimitsOfShape J (AsSmall C) holds as well.

Русский

Если для формы J выполнено HasLimitsOfShape J C, то и HasLimitsOfShape J (AsSmall C).

LaTeX

$$$\forall J\, [\mathbf{Category} J]\, [\operatorname{HasLimitsOfShape} J\, C],\; \operatorname{HasLimitsOfShape} J\; (\mathrm{AsSmall}\, C)$$

Lean4

instance hasLimitsOfShape (J : Type*) [Category J] [HasLimitsOfShape J C] :
    HasLimitsOfShape.{_, _, max u v w} J (AsSmall.{w} C) :=
  Adjunction.hasLimitsOfShape_of_equivalence equiv.inverse

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