finCategoryWidePullback

Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

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

English

WidePullbackShape J forms a finite category when J is finite.

Русский

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

LaTeX

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

Lean4

instance finCategoryWidePullback [Fintype J] : FinCategory (WidePullbackShape J) where
  fintypeHom := WidePullbackShape.fintypeHom

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

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

Разделы

Аффилиация

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