bind_pmap — Mathlib

English

A distributive property of bind over pmap: bind (Option.pmap f x H) g equals x.pbind (λ a h, g (f a (H a h))).

Русский

Свойство распределения связывания над pmap: bind (Option.pmap f x H) g = x.pbind (λ a h, g (f a (H a h))).

LaTeX

$$$$ \operatorname{bind}(\operatorname{Option}.pmap f x H, g) = x.\mathrm{pbind}(\lambda a h, g (f a (H a h))). $$$$

Lean4

theorem bind_pmap {α β γ} {p : α → Prop} (f : ∀ a, p a → β) (x : Option α) (g : β → Option γ) (H) :
    pmap f x H >>= g = x.pbind fun a h ↦ g (f a (H _ h)) := by grind [cases Option, pmap]

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