TypeVec

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec

English

n-tuples of types, as a category; TypeVec n is defined as Fin2 n → Type.

Русский

n-кортежи типов, образующие категорию; TypeVec(n) определяется как Fin2(n) → Type.

LaTeX

$$$\\text{TypeVec}(n) = \\mathrm{Fin}_2(n) \\to \\mathrm{Type}$$$

Lean4

/-- n-tuples of types, as a category -/
@[pp_with_univ]
def TypeVec (n : ℕ) :=
  Fin2 n → Type*

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

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

Разделы

Аффилиация

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