apply Measure.lintegral_bind (is_measurable hf) hφ
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.5239
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
φ : Y → ℝ≥0∞
hf : Measurable f
hφ : Measurable φ
⊢ (∫⁻ (x' : Y), φ x' ∂Measure.bind ↑x.μ fun x => ↑(f x).μ) = ∫⁻ (x' : X), ∫⁻ (x' : Y), φ x' ∂↑(f x').μ ∂↑x.μ
no goals