map

Mathlib.Data.QPF.Multivariate.Constructions.Const

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

English

The map on a constant functor is identity: Constrant maps to itself unchanged by f.

Русский

Отображение константного функторa оставляет значение без изменений под действием f.

LaTeX

$$$\mathrm{Const.map}(f)(\mathrm{Const.mk}(a)) = \mathrm{Const.mk}(a).$$$

Lean4

/-- `map` for constant functor -/
protected def map : Const n A α → Const n A β := fun x => x

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

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

Разделы

Аффилиация

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