α : Type u_1
α' : Type ?u.2462095
β : Type u_2
β' : Type ?u.2462101
γ : Type ?u.2462104
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.2462369
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : α × β → E
s : Set α
t : Set β
hf : Integrable f
⊢ (∫ (z : α × β) in s ×ˢ t, f z ∂Measure.prod μ ν) = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
α : Type u_1
α' : Type ?u.2462095
β : Type u_2
β' : Type ?u.2462101
γ : Type ?u.2462104
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.2462369
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : α × β → E
s : Set α
t : Set β
hf : IntegrableOn f (s ×ˢ t)
⊢ (∫ (z : α × β) in s ×ˢ t, f z ∂Measure.prod μ ν) = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
simp only [← Measure.prod_restrict s t, IntegrableOn] at hf ⊢
α : Type u_1
α' : Type ?u.2462095
β : Type u_2
β' : Type ?u.2462101
γ : Type ?u.2462104
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.2462369
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : α × β → E
s : Set α
t : Set β
hf : Integrable f
⊢ (∫ (z : α × β), f z ∂Measure.prod (Measure.restrict μ s) (Measure.restrict ν t)) =
    ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
α : Type u_1
α' : Type ?u.2462095
β : Type u_2
β' : Type ?u.2462101
γ : Type ?u.2462104
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.2462369
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : α × β → E
s : Set α
t : Set β
hf : Integrable f
⊢ (∫ (z : α × β) in s ×ˢ t, f z ∂Measure.prod μ ν) = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
rw [← Measure.prod_restrict s t] at hf ⊢
no goals
α : Type u_1
α' : Type ?u.2462095
β : Type u_2
β' : Type ?u.2462101
γ : Type ?u.2462104
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.2462369
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : α × β → E
s : Set α
t : Set β
hf : Integrable f
⊢ (∫ (z : α × β), f z ∂Measure.prod (Measure.restrict μ s) (Measure.restrict ν t)) =
    ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
exact integral_prod f hf