hasLimitsOfShape — Mathlib

English

For any shape J, if C has limits of shape J, then ShrinkHoms C has limits of shape J.

Русский

Для любой формы J, если C имеет пределы формы J, то ShrinkHoms C имеет пределы формы J.

LaTeX

$$$\forall J,\ HasLimitsOfShape J C \Rightarrow HasLimitsOfShape J (ShrinkHoms C)$$$

Lean4

instance hasLimitsOfShape (J : Type*) [Category J] [HasLimitsOfShape J C] :
    HasLimitsOfShape.{_, _, w} J (ShrinkHoms C) :=
  Adjunction.hasLimitsOfShape_of_equivalence (inverse C)

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