asTypeFinCategory

Mathlib.CategoryTheory.FinCategory.AsType

URI: https://scilib.ai/kg/mathlib#CategoryTheory.FinCategory.asTypeFinCategory

English

The constructed instance provides a FinCategory structure on AsType(α).

Русский

Сконструированный инстанс наделяет AsType(α) структурой FinCategory.

LaTeX

$$$\\text{asTypeFinCategory}(\\alpha) : \\mathrm{FinCategory}(\\mathrm{AsType}(\\alpha))$$$

Lean4

noncomputable instance asTypeFinCategory : FinCategory (AsType α) where
  fintypeHom := fun _ _ => show Fintype (Fin _) from inferInstance

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

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

Разделы

Аффилиация

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