α : Type u_3
β✝ : Type ?u.135307
E : Type u_2
F : Type ?u.135313
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g✝ : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
β : Type u_1
inst✝ : MeasurableSpace β
g : α → β
f : β → E
s : Set β
hs : MeasurableSet s
hf : AEStronglyMeasurable f (Measure.map g μ)
hg : AEMeasurable g
⊢ Measure.map g (Measure.restrict μ (g ⁻¹' s)) ≤ Measure.map g μ
α : Type u_3
β✝ : Type ?u.135307
E : Type u_2
F : Type ?u.135313
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g✝ : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
β : Type u_1
inst✝ : MeasurableSpace β
g : α → β
f : β → E
s : Set β
hs : MeasurableSet s
hf : AEStronglyMeasurable f (Measure.map g μ)
hg : AEMeasurable g
⊢ (∫ (y : β) in s, f y ∂Measure.map g μ) = ∫ (x : α) in g ⁻¹' s, f (g x) ∂μ
rw [Measure.restrict_map_of_aemeasurable hg hs,
  integral_map (hg.mono_measure Measure.restrict_le_self) (hf.mono_measure _)]
no goals
α : Type u_3
β✝ : Type ?u.135307
E : Type u_2
F : Type ?u.135313
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f✝ g✝ : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
β : Type u_1
inst✝ : MeasurableSpace β
g : α → β
f : β → E
s : Set β
hs : MeasurableSet s
hf : AEStronglyMeasurable f (Measure.map g μ)
hg : AEMeasurable g
⊢ Measure.map g (Measure.restrict μ (g ⁻¹' s)) ≤ Measure.map g μ
exact Measure.map_mono_of_aemeasurable Measure.restrict_le_self hg