hasFiniteColimits_of_hasColimits — Mathlib

English

If HasColimitsOfSize.{0,0} C, then HasFiniteColimits C.

Русский

Если в C существуют конечные колимиты в нулевом размере, то имеются конечные колимиты.

LaTeX

$$$\operatorname{HasColimitsOfSize}_{0,0}(C) \Rightarrow \operatorname{HasFiniteColimits}(C)$$$

Lean4

instance (priority := 100) hasFiniteColimits_of_hasColimits [HasColimits C] : HasFiniteColimits C :=
  hasFiniteColimits_of_hasColimitsOfSize C

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