ext
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
⊢ bind (bind x g) f = bind x fun x' => bind (g x') f
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
s✝ : Set Z
a✝ : MeasurableSet s✝
⊢ ↑↑↑(bind (bind x g) f).μ s✝ = ↑↑↑(bind x fun x' => bind (g x') f).μ s✝