Theorems · Theorem

PMF.bind_bind

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (f : α → PMF β) (g : β → PMF γ),
  (p.bind f).bind g = p.bind fun a => (f a).bind g

Defined in

Mathlib.Probability.ProbabilityMassFunction.Monad

Cited by

3 results in Mathlib

Foundations

Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound