mvfunctor

Mathlib.Data.QPF.Multivariate.Constructions.Fix

URI: https://scilib.ai/kg/mathlib#MvQPF.Fix.mvfunctor

English

There is a natural MvFunctor structure on Fix F, with map equal to Fix.map.

Русский

Существует естественная структура MvFunctor на Fix F, отображение равно Fix.map.

LaTeX

$$$\text{mvfunctor} : MvFunctor (Fix F) \quad\text{with } \mathrm{map} := \mathrm{Fix.map}$$$

Lean4

instance mvfunctor : MvFunctor (Fix F) where map := Fix.map

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

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

Разделы

Аффилиация

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