discreteFintype

Mathlib.CategoryTheory.FinCategory.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.discreteFintype

English

For any α with a finite type, the discrete category on α is finite.

Русский

Для любого α с конечным типом дискретная категория на α является конечной.

LaTeX

$$$[\\text{Fintype } \\alpha] \\\\Rightarrow \\\\operatorname{Fintype}(\\operatorname{Discrete}(\\alpha)).$$$

Lean4

instance discreteFintype {α : Type*} [Fintype α] : Fintype (Discrete α) :=
  Fintype.ofEquiv α discreteEquiv.symm

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

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

Разделы

Аффилиация

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