pmap_bind_id_eq_pmap_join

Mathlib.Data.Option.Basic

URI: https://scilib.ai/kg/mathlib#Option.pmap_bind_id_eq_pmap_join

Lean4

theorem pmap_bind_id_eq_pmap_join {f : ∀ a, p a → β} {x : Option (Option α)} (H) :
    ((pmap (pmap f) x H).bind fun a ↦ a) = pmap f x.join fun a h ↦ H (some a) (mem_of_mem_join h) _ rfl := by
  grind [cases Option]

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

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

Разделы

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

Аффилиация

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