mvfunctorW

Mathlib.Data.PFunctor.Multivariate.W

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

English

Equip the W-type P with a multivariate functor structure by providing a standard instance of MvFunctor on W; i.e., W carries a functorial action.

Русский

Обозначим W-переменную структуру на типе W; W обладает действием функторной структуры.

LaTeX

$$$\text{instance } mvfunctorW : MvFunctor P.W$$$

Lean4

instance mvfunctorW : MvFunctor P.W := by delta MvPFunctor.W; infer_instance

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

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

Разделы

Аффилиация

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