AsType

Mathlib.CategoryTheory.FinCategory.AsType

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

English

The type AsType α is a finite-type surrogate for α.

Русский

Тип AsType α служит конечнопородным эквивалентом α.

LaTeX

$$$\\text{AsType}(\\alpha) = \\text{Fin}(\\lvert α\\rvert)$$$

Lean4

/-- A FinCategory `α` is equivalent to a fin_category with in `Type`. -/
--@[nolint unused_arguments]

abbrev AsType : Type :=
  Fin (Fintype.card α)

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

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

Разделы

Аффилиация

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