α : Type u_2
α' : Type ?u.2385081
β : Type u_3
β' : Type ?u.2385087
γ✝ : Type ?u.2385090
E : Type ?u.2385093
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ✝
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ✝
inst✝³ : NormedAddCommGroup E
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
f : β × α → γ
hf : AEStronglyMeasurable f (map Prod.swap (Measure.prod μ ν))
⊢ AEStronglyMeasurable (fun z => f (Prod.swap z)) (Measure.prod μ ν)
α : Type u_2
α' : Type ?u.2385081
β : Type u_3
β' : Type ?u.2385087
γ✝ : Type ?u.2385090
E : Type ?u.2385093
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ✝
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ✝
inst✝³ : NormedAddCommGroup E
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
f : β × α → γ
hf : AEStronglyMeasurable f (Measure.prod ν μ)
⊢ AEStronglyMeasurable (fun z => f (Prod.swap z)) (Measure.prod μ ν)
rw [← prod_swap] at hf
no goals
α : Type u_2
α' : Type ?u.2385081
β : Type u_3
β' : Type ?u.2385087
γ✝ : Type ?u.2385090
E : Type ?u.2385093
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ✝
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ✝
inst✝³ : NormedAddCommGroup E
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
f : β × α → γ
hf : AEStronglyMeasurable f (map Prod.swap (Measure.prod μ ν))
⊢ AEStronglyMeasurable (fun z => f (Prod.swap z)) (Measure.prod μ ν)
exact hf.comp_measurable measurable_swap