map_comp_map

Mathlib.Control.Functor

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

Lean4

theorem map_comp_map (f : α → β) (g : β → γ) : ((g <$> ·) ∘ (f <$> ·) : F α → F γ) = ((g ∘ f) <$> ·) :=
  funext fun _ => (comp_map _ _ _).symm

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

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

Разделы

Аффилиация

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