hasLimitsOfShape_thinSkeleton — Mathlib

English

If J has limits in C, then the ThinSkeleton of C has the same J-shaped limits, provided C is a category.

Русский

Если у C существуют пределы формы J, то у ThinSkeleton(C) существуют такие же пределы формы J при условии, что C является категорией.

LaTeX

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

Lean4

instance hasLimitsOfShape_thinSkeleton [HasLimitsOfShape J C] : HasLimitsOfShape J (ThinSkeleton C) :=
  hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (fromThinSkeleton C)

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