hasFiniteColimits — Mathlib

English

The category FinTypeCat of finite types has finite colimits; that is, for every finite diagram there exists a colimit in FinTypeCat.

Русский

Категория FinTypeCat конечных типов имеет все конечные ко-лимиты; для каждого конечного диаграммного объекта существует ко-лимит в FinTypeCat.

LaTeX

$$$\\text{HasFiniteColimits } \\mathrm{FintypeCat}$$$

Lean4

instance hasFiniteColimits : HasFiniteColimits FintypeCat.{u} where out _ := inferInstance

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