map_bind — Mathlib

English

For PMF p on α, a family q : α → PMF β, and a function f : β → γ, the image of p.bind q under map f equals p.bind (λ a, (q a).map f).

Русский

Для PMF p на α, семейства q : α → PMF β и функции f : β → γ, образ p.bind q под отображением f равен p.bind (λ a, (q a).map f).

LaTeX

$$$ PMF.map f (PMF.bind p q) = PMF.bind (p) (fun a => PMF.map f (q a)) $$$

Lean4

theorem map_bind (q : α → PMF β) (f : β → γ) : (p.bind q).map f = p.bind fun a => (q a).map f :=
  bind_bind _ _ _

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