α : Type u_2
α' : Type ?u.2467745
β : Type u_3
β' : Type ?u.2467751
γ : Type ?u.2467754
E : Type ?u.2467757
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.2468019
inst✝³ : NormedAddCommGroup E'
inst✝² : CompleteSpace E'
inst✝¹ : NormedSpace ℝ E'
L : Type u_1
inst✝ : IsROrC L
f : α → L
g : β → L
s : Set α
t : Set β
⊢ (∫ (z : α × β), f z.fst * g z.snd ∂Measure.prod (Measure.restrict μ s) (Measure.restrict ν t)) =
    (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν
α : Type u_2
α' : Type ?u.2467745
β : Type u_3
β' : Type ?u.2467751
γ : Type ?u.2467754
E : Type ?u.2467757
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.2468019
inst✝³ : NormedAddCommGroup E'
inst✝² : CompleteSpace E'
inst✝¹ : NormedSpace ℝ E'
L : Type u_1
inst✝ : IsROrC L
f : α → L
g : β → L
s : Set α
t : Set β
⊢ (∫ (z : α × β) in s ×ˢ t, f z.fst * g z.snd ∂Measure.prod μ ν) = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν
rw [← Measure.prod_restrict s t]
no goals
α : Type u_2
α' : Type ?u.2467745
β : Type u_3
β' : Type ?u.2467751
γ : Type ?u.2467754
E : Type ?u.2467757
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.2468019
inst✝³ : NormedAddCommGroup E'
inst✝² : CompleteSpace E'
inst✝¹ : NormedSpace ℝ E'
L : Type u_1
inst✝ : IsROrC L
f : α → L
g : β → L
s : Set α
t : Set β
⊢ (∫ (z : α × β), f z.fst * g z.snd ∂Measure.prod (Measure.restrict μ s) (Measure.restrict ν t)) =
    (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν
simp only [← Measure.prod_restrict s t, IntegrableOn, integral_prod_mul]