mapConstRev

Mathlib.Control.Functor

URI: https://scilib.ai/kg/mathlib#Functor.mapConstRev

Lean4

/-- If `f` is a functor, if `fb : f β` and `a : α`, then `mapConstRev fb a` is the result of
  applying `f.map` to the constant function `β → α` sending everything to `a`, and then
  evaluating at `fb`. In other words it's `const a <$> fb`. -/
abbrev mapConstRev {f : Type u → Type v} [Functor f] {α β : Type u} : f β → α → f α := fun a b => Functor.mapConst b a

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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