hasColimitsOfShape_skeleton — Mathlib

English

If J-shaped colimits exist in C, then J-shaped colimits exist in Skeleton(C).

Русский

Если в C существуют колимиты формы J, то и в Skeleton(C) существуют колимиты формы J.

LaTeX

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

Lean4

instance hasColimitsOfShape_skeleton [HasColimitsOfShape J C] : HasColimitsOfShape J (Skeleton C) :=
  hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape (fromSkeleton C)

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