α : Type u_1
α' : Type ?u.4544974
β : Type u_2
β' : Type ?u.4544980
γ : Type u_3
E : Type ?u.4544986
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
f : β × α → γ
hf : AEMeasurable f
⊢ AEMeasurable fun z => f (Prod.swap z)
α : Type u_1
α' : Type ?u.4544974
β : Type u_2
β' : Type ?u.4544980
γ : Type u_3
E : Type ?u.4544986
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
f : β × α → γ
hf : AEMeasurable f
⊢ AEMeasurable fun z => f (Prod.swap z)
rw [← Measure.prod_swap] at hf
no goals
α : Type u_1
α' : Type ?u.4544974
β : Type u_2
β' : Type ?u.4544980
γ : Type u_3
E : Type ?u.4544986
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
f : β × α → γ
hf : AEMeasurable f
⊢ AEMeasurable fun z => f (Prod.swap z)
exact hf.comp_measurable measurable_swap