finCategoryWidePushout

Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

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

English

WidePushoutShape J is a finite category when J is finite.

Русский

WidePushoutShape J образует конечную категорию, если J конечен.

LaTeX

$$$\operatorname{FinCategory}(\mathrm{WidePushoutShape}(J))$$$

Lean4

instance finCategoryWidePushout [Fintype J] : FinCategory (WidePushoutShape J) where
  fintypeHom := WidePushoutShape.fintypeHom

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

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

Разделы

Аффилиация

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