seq_mk

Mathlib.Control.Applicative

URI: https://scilib.ai/kg/mathlib#Comp.seq_mk

Lean4

@[functor_norm]
theorem seq_mk {α β : Type w} {f : Type u → Type v} {g : Type w → Type u} [Applicative f] [Applicative g]
    (h : f (g (α → β))) (x : f (g α)) : Comp.mk h <*> Comp.mk x = Comp.mk ((· <*> ·) <$> h <*> x) :=
  rfl

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

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

Разделы

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

Аффилиация

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