α : Type u_2
α' : Type ?u.4457703
β : Type u_1
β' : Type ?u.4457709
γ : Type ?u.4457712
E : Type ?u.4457715
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ (∫⁻ (x : β), ↑↑μ (Prod.mk x ⁻¹' (Prod.swap ⁻¹' s)) ∂ν) = ∫⁻ (y : β), ↑↑μ ((fun x => (x, y)) ⁻¹' s) ∂ν
α : Type u_2
α' : Type ?u.4457703
β : Type u_1
β' : Type ?u.4457709
γ : Type ?u.4457712
E : Type ?u.4457715
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ ↑↑(Measure.prod μ ν) s = ∫⁻ (y : β), ↑↑μ ((fun x => (x, y)) ⁻¹' s) ∂ν
rw [← prod_swap, map_apply measurable_swap hs, prod_apply (measurable_swap hs)]
no goals
α : Type u_2
α' : Type ?u.4457703
β : Type u_1
β' : Type ?u.4457709
γ : Type ?u.4457712
E : Type ?u.4457715
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ (∫⁻ (x : β), ↑↑μ (Prod.mk x ⁻¹' (Prod.swap ⁻¹' s)) ∂ν) = ∫⁻ (y : β), ↑↑μ ((fun x => (x, y)) ⁻¹' s) ∂ν
rfl