Theorems · Theorem

PMF.bindOnSupport_apply

∀ {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β) (b : β),
  (p.bindOnSupport f) b = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b

Defined in

Mathlib.Probability.ProbabilityMassFunction.Monad

Cited by

1 results in Mathlib

Foundations

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