monadLift_bind

Mathlib.Control.Monad.Cont

URI: https://scilib.ai/kg/mathlib#ContT.monadLift_bind

Lean4

theorem monadLift_bind [Monad m] [LawfulMonad m] {α β} (x : m α) (f : α → m β) :
    (monadLift (x >>= f) : ContT r m β) = monadLift x >>= monadLift ∘ f :=
  by
  ext
  simp only [monadLift, (· ∘ ·), (· >>= ·), bind_assoc, id, run, ContT.monadLift]

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

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

Разделы

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

Аффилиация

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