α : Type u_1
α' : Type ?u.4488691
β : Type u_2
β' : Type ?u.4488697
γ : Type ?u.4488700
E : Type ?u.4488703
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set α
this : ν = restrict ν univ
⊢ Measure.prod (restrict μ s) ν = restrict (Measure.prod μ ν) (s ×ˢ univ)
α : Type u_1
α' : Type ?u.4488691
β : Type u_2
β' : Type ?u.4488697
γ : Type ?u.4488700
E : Type ?u.4488703
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set α
⊢ Measure.prod (restrict μ s) ν = restrict (Measure.prod μ ν) (s ×ˢ univ)
have : ν = ν.restrict Set.univ := Measure.restrict_univ.symm
no goals
α : Type u_1
α' : Type ?u.4488691
β : Type u_2
β' : Type ?u.4488697
γ : Type ?u.4488700
E : Type ?u.4488703
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set α
this : ν = restrict ν univ
⊢ Measure.prod (restrict μ s) ν = restrict (Measure.prod μ ν) (s ×ˢ univ)
rw [this, Measure.prod_restrict, ← this]