fintypeObj

Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

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

English

If J is finite, then the objects of WidePullbackShape J form a finite type.

Русский

Если J конечно, то множества объектов WidePullbackShape J формируют конечный тип.

LaTeX

$$$\text{Fintype}(\mathrm{WidePullbackShape}(J))$$$

Lean4

instance fintypeObj [Fintype J] : Fintype (WidePushoutShape J) :=
  inferInstanceAs <| Fintype (Option _)

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

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

Разделы

Аффилиация

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