instFintypeHomObjAsType

Mathlib.CategoryTheory.FinCategory.AsType

URI: https://scilib.ai/kg/mathlib#CategoryTheory.FinCategory.instFintypeHomObjAsType

English

The Hom-sets in the FinCategory for ObjAsType α are finite.

Русский

Множества Hom в FinCategory для ObjAsType α конечны.

LaTeX

$$$\\text{Fintype}(\\mathrm{Hom}_{\\mathrm{ObjAsType}(\\alpha)}(X,Y))$$$

Lean4

instance {i j : ObjAsType α} : Fintype (i ⟶ j) :=
  FinCategory.fintypeHom ((Fintype.equivFin α).symm i) _

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

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

Разделы

Аффилиация

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