case h
α : Type u_2
α' : Type ?u.2479556
β : Type u_1
β' : Type ?u.2479562
γ : Type ?u.2479565
E : Type ?u.2479568
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b => ↑↑(map (Prod.mk b) ν) s
α : Type u_2
α' : Type ?u.2479556
β : Type u_1
β' : Type ?u.2479562
γ : Type ?u.2479565
E : Type ?u.2479568
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
⊢ Measurable fun x => map (Prod.mk x) ν
apply measurable_of_measurable_coe
case h
α : Type u_2
α' : Type ?u.2479556
β : Type u_1
β' : Type ?u.2479562
γ : Type ?u.2479565
E : Type ?u.2479568
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(map (Prod.mk b) ν) s
case h
α : Type u_2
α' : Type ?u.2479556
β : Type u_1
β' : Type ?u.2479562
γ : Type ?u.2479565
E : Type ?u.2479568
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
⊢ ∀ (s : Set (α × β)), MeasurableSet s → Measurable fun b => ↑↑(map (Prod.mk b) ν) s
intro s hs
case h
α : Type u_2
α' : Type ?u.2479556
β : Type u_1
β' : Type ?u.2479562
γ : Type ?u.2479565
E : Type ?u.2479568
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑ν (Prod.mk b ⁻¹' s)
case h
α : Type u_2
α' : Type ?u.2479556
β : Type u_1
β' : Type ?u.2479562
γ : Type ?u.2479565
E : Type ?u.2479568
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(map (Prod.mk b) ν) s
simp_rw [map_apply measurable_prod_mk_left hs]
no goals
case h
α : Type u_2
α' : Type ?u.2479556
β : Type u_1
β' : Type ?u.2479562
γ : Type ?u.2479565
E : Type ?u.2479568
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑ν (Prod.mk b ⁻¹' s)
exact measurable_measure_prod_mk_left hs