M

Mathlib.Data.PFunctor.Multivariate.M

URI: https://scilib.ai/kg/mathlib#MvPFunctor.M

English

The n+1-ary functor M sends α to the M-type of P, yielding a new multivariate functor M with arity n and index type α.

Русский

Функтор M преобразует n+1-арный функтор в M‑тип, создавая новый мультфунктор с арностью n и индексным типом α.

LaTeX

$$$M(α) = P.mp(α)$$$

Lean4

/-- `n`-ary M-type for `P` -/
def M (α : TypeVec n) : Type _ :=
  P.mp α

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

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

Разделы

Аффилиация

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