hasColimitsOfSize_skeleton — Mathlib

English

If C has colimits of size {w, w'}, then Skeleton(C) has colimits of size {w, w'}.

Русский

Если у C существуют колимиты размера {w, w'}, то у Skeleton(C) существуют колимиты такого же размера.

LaTeX

$$$\\forall \\{w,w'\\}, \\text{HasColimitsOfSize } \\{w, w'\\} C \\Rightarrow HasColimitsOfSize \\{w, w'\\} (\\mathrm{Skeleton}\\;C)$$$

Lean4

instance hasColimitsOfSize_skeleton [HasColimitsOfSize.{w, w'} C] : HasColimitsOfSize.{w, w'} (Skeleton C) :=
  hasColimits_of_hasColimits_createsColimits (fromSkeleton C)

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