hasLimitsOfShape_skeleton — Mathlib

English

If a category C has all limits of shape J, then the skeleton of C has all limits of shape J.

Русский

Если категория C имеет пределы формы J, то скелет этой категории Skeleton(C) имеет пределы формы J.

LaTeX

$$$\\forall J\\, \\text{HasLimitsOfShape } J C \\Rightarrow \\text{HasLimitsOfShape } J (\\mathrm{Skeleton}\\;C)$$$

Lean4

instance hasLimitsOfShape_skeleton [HasLimitsOfShape J C] : HasLimitsOfShape J (Skeleton C) :=
  hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (fromSkeleton C)

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