Prj

Mathlib.Data.QPF.Multivariate.Constructions.Prj

URI: https://scilib.ai/kg/mathlib#MvQPF.Prj

English

Projection functor: given a finite vector of types v, the i-th component is selected as the projection Prj(v) = v i.

Русский

Проекция: из вектора типов выбирается i-й компонент.

LaTeX

$$$\mathrm{Prj}(v) := v(i)$$$

Lean4

/-- The projection `i` functor -/
def Prj (v : TypeVec.{u} n) : Type u :=
  v i

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

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

Разделы

Аффилиация

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