finite

Mathlib.CategoryTheory.Comma.CardinalArrow

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Arrow.finite

English

If C is a finite category, then Arrow C is finite.

Русский

Если C — конечная категория, то Arrow C конечна.

LaTeX

$$$\\\\operatorname{Finite}(\\\\operatorname{Arrow}(C))$$$

Lean4

instance finite {C : Type u} [SmallCategory C] [FinCategory C] : Finite (Arrow C) :=
  by
  rw [Arrow.finite_iff]
  exact ⟨inferInstance⟩

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

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

Разделы

Аффилиация

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