instPreservesFiniteColimitsFintypeCatForget

Mathlib.CategoryTheory.Limits.FintypeCat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForget

English

The forgetful functor from FintypeCat preserves finite colimits.

Русский

Функтор забывания из FintypeCat сохраняет конечные колимиты.

LaTeX

$$$\\mathrm{PreservesFiniteColimits}(\\mathrm{forget}\\, \\mathrm{FintypeCat})$$$

Lean4

noncomputable instance : PreservesFiniteColimits (forget FintypeCat) :=
  FintypeCat.inclusion_preservesFiniteColimits

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru