English
Under suitable hypotheses, pmap interacts with bind via a distributive law: pmap f x H >>= g equals x >>= (a ↦ pmap f (g a) (λ _, H a ‹_›)).
Русский
При подходящих предположениях pmap и bind взаимодействуют по закону распределения: pmap f x H >>= g = x >>= (a ↦ pmap f (g a) (λ _, H a h)).
LaTeX
$$$$ \text{pmap_bind} \; (f) (x) (g) (p) (H) \;=\; x \gg= \lambda a, \; \text{pmap } f (g a) (\lambda _, H a _). $$$$
Lean4
theorem pmap_bind {α β γ} {x : Option α} {g : α → Option β} {p : β → Prop} {f : ∀ b, p b → γ} (H)
(H' : ∀ (a : α), ∀ b ∈ g a, b ∈ x >>= g) :
pmap f (x >>= g) H = x >>= fun a ↦ pmap f (g a) fun _ h ↦ H _ (H' a _ h) := by grind [cases Option]
