hasColimitsOfSize_thinSkeleton — Mathlib

English

If a category C has colimits of a given size (HasColimitsOfSize {w, w'} C), then ThinSkeleton C has colimits of that same size.

Русский

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

LaTeX

$$$\mathrm{HasColimitsOfSize}^{\{w,w'\}}(J,C) \Rightarrow \mathrm{HasColimitsOfSize}^{\{w,w'\}}(J,\mathrm{ThinSkeleton}(C))$$$

Lean4

instance hasColimitsOfSize_thinSkeleton [HasColimitsOfSize.{w, w'} C] : HasColimitsOfSize.{w, w'} (ThinSkeleton C) :=
  hasColimits_of_hasColimits_createsColimits (fromThinSkeleton C)

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