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