Theorems · Definition

PMF.bindOnSupport

{α : Type u_1} → {β : Type u_2} → (p : PMF α) → ((a : α) → a ∈ p.support → PMF β) → PMF β

Generalized version of bind allowing f to only be defined on the support of p. p.bind f is equivalent to p.bindOnSupport (fun a _ ↦ f a), see bindOnSupport_eq_bind.

Defined in

Mathlib.Probability.ProbabilityMassFunction.Monad

Cited by

11 results in Mathlib

Foundations

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