instHasLimitsOfShapeWalkingParallelPairInd

English

If C has limits of shape WalkingParallelPair, then Ind(C) has limits of shape WalkingParallelPair as well.

Русский

Если в C есть пределы формы WalkingParallelPair, то и Ind(C) имеет пределы формы WalkingParallelPair.

LaTeX

$$$[HasLimitsOfShape WalkingParallelPair C] \\Rightarrow [HasLimitsOfShape WalkingParallelPair (Ind C)]$$$

Lean4

instance [HasLimitsOfShape WalkingParallelPair C] : HasLimitsOfShape WalkingParallelPair (Ind C) :=
  hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (Ind.inclusion C)

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