traverse_comp

Mathlib.Control.Traversable.Lemmas

URI: https://scilib.ai/kg/mathlib#Traversable.traverse_comp

Lean4

@[functor_norm]
theorem traverse_comp (g : α → F β) (h : β → G γ) :
    traverse (Comp.mk ∘ map h ∘ g) = (Comp.mk ∘ map (traverse h) ∘ traverse g : t α → Comp F G (t γ)) :=
  by
  ext
  exact comp_traverse _ _ _

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

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

Разделы

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

Аффилиация

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