funext y
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.44890
inst✝¹ : MeasurableSpace Z
R : Type ?u.44896
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
⊢ rpdf (bind x f) ν = fun y => ∫ (x' : X), rpdf (f x') ν y ∂↑x.μ
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.44890
inst✝¹ : MeasurableSpace Z
R : Type ?u.44896
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ rpdf (bind x f) ν y = ∫ (x' : X), rpdf (f x') ν y ∂↑x.μ