MvFunctor

Mathlib.Data.QPF.Multivariate.Constructions.Const

URI: https://scilib.ai/kg/mathlib#MvQPF.Const.MvFunctor

English

The Const functor is equipped with a multivariate functor structure, with map defined by Const.map.

Русский

Для Const задаётся структура мультфункторности, отображение задано как Const.map.

LaTeX

$$$\text{MvFunctor} (\mathrm{Const}\; n\; A) \text{ with } \mathrm{map} = \mathrm{Const.map}.$$$

Lean4

instance MvFunctor : MvFunctor (Const n A) where map _f := Const.map

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

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

Разделы

Аффилиация

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