α : Type u_2
α' : Type ?u.2378632
β : Type u_1
β' : Type ?u.2378638
γ : Type ?u.2378641
E : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SigmaFinite ν
f : α × β → E
hf : StronglyMeasurable (uncurry (curry f))
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν
α : Type u_2
α' : Type ?u.2378632
β : Type u_1
β' : Type ?u.2378638
γ : Type ?u.2378641
E : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SigmaFinite ν
f : α × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν
rw [← uncurry_curry f] at hf
no goals
α : Type u_2
α' : Type ?u.2378632
β : Type u_1
β' : Type ?u.2378638
γ : Type ?u.2378641
E : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SigmaFinite ν
f : α × β → E
hf : StronglyMeasurable (uncurry (curry f))
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν
exact hf.integral_prod_right