α : Type u_1
α' : Type ?u.2413828
β : Type u_2
β' : Type ?u.2413834
γ : Type ?u.2413837
E : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MeasurableSpace α'
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace β'
inst✝⁵ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SigmaFinite ν
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SigmaFinite μ
f : α × β → E
hf : AEStronglyMeasurable f (map Prod.swap (Measure.prod ν μ))
⊢ (∫ (z : β × α), f (Prod.swap z) ∂Measure.prod ν μ) = ∫ (z : α × β), f z ∂Measure.prod μ ν
α : Type u_1
α' : Type ?u.2413828
β : Type u_2
β' : Type ?u.2413834
γ : Type ?u.2413837
E : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MeasurableSpace α'
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace β'
inst✝⁵ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SigmaFinite ν
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SigmaFinite μ
f : α × β → E
hf : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ (∫ (z : β × α), f (Prod.swap z) ∂Measure.prod ν μ) = ∫ (z : α × β), f z ∂Measure.prod μ ν
rw [← prod_swap] at hf
no goals
α : Type u_1
α' : Type ?u.2413828
β : Type u_2
β' : Type ?u.2413834
γ : Type ?u.2413837
E : Type u_3
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MeasurableSpace α'
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace β'
inst✝⁵ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SigmaFinite ν
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SigmaFinite μ
f : α × β → E
hf : AEStronglyMeasurable f (map Prod.swap (Measure.prod ν μ))
⊢ (∫ (z : β × α), f (Prod.swap z) ∂Measure.prod ν μ) = ∫ (z : α × β), f z ∂Measure.prod μ ν
rw [← integral_map measurable_swap.aemeasurable hf, prod_swap]