W

Mathlib.Data.PFunctor.Multivariate.W

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

English

Definition of W: the W-type object associated to P is the same as P.wp; it collects trees with labeled paths as described by P.

Русский

Определение W: связанный W-тип объекта для P равен P.wp; он собирает деревья с помеченными путями согласно P.

LaTeX

$$$W (\alpha) := P.wp \alpha$$$

Lean4

/-- W-type of `P` -/
def W (α : TypeVec n) : Type _ :=
  P.wp α

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

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

Разделы

Аффилиация

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