instReflectsFiniteColimitsOfReflectsColimitsOfSize

English

If F reflects colimits of size (w,w2), then F reflects finite colimits.

Русский

Если F отражает колимиты заданного размера (w,w2), тогда F отражает конечные колимиты.

LaTeX

$$$\mathrm{ReflectsColimitsOfSize}(F) \Rightarrow \mathrm{ReflectsFiniteColimits}(F)$$$

Lean4

instance (priority := 120) (F : C ⥤ D) [ReflectsColimitsOfSize.{0, 0} F] : ReflectsFiniteColimits F :=
  ReflectsColimitsOfSize.reflectsFiniteColimits F

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