α : Type u_1
α' : Type ?u.2456513
β : Type u_2
β' : Type ?u.2456519
γ : Type ?u.2456522
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 μ
E' : Type ?u.2456787
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : α × β → E
hf : Integrable f
⊢ (∫ (z : β × α), f (Prod.swap z) ∂Measure.prod ν μ) = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
α : Type u_1
α' : Type ?u.2456513
β : Type u_2
β' : Type ?u.2456519
γ : Type ?u.2456522
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 μ
E' : Type ?u.2456787
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : α × β → E
hf : Integrable f
⊢ (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
simp_rw [← integral_prod_swap f hf.aestronglyMeasurable]
no goals
α : Type u_1
α' : Type ?u.2456513
β : Type u_2
β' : Type ?u.2456519
γ : Type ?u.2456522
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 μ
E' : Type ?u.2456787
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : α × β → E
hf : Integrable f
⊢ (∫ (z : β × α), f (Prod.swap z) ∂Measure.prod ν μ) = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
exact integral_prod _ hf.swap