instCommApplicative

Mathlib.Control.Applicative

URI: https://scilib.ai/kg/mathlib#Functor.Comp.instCommApplicative

Lean4

instance {f : Type u → Type w} {g : Type v → Type u} [Applicative f] [Applicative g] [CommApplicative f]
    [CommApplicative g] : CommApplicative (Comp f g) where
  commutative_prod _
    _ := by
    simp! [map, Seq.seq]
    rw [commutative_map]
    simp only [mk, flip, seq_map_assoc, Function.comp_def, map_map]
    congr
    funext x y
    rw [commutative_map]
    congr

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

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

Разделы

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

Аффилиация

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