α : Type u_1
β : Type u_2
γ : Type ?u.44831
f : α → β
p : Pmf α
b : β
s : Set β
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ ↑(toOuterMeasure (map f p)) s = ↑(toOuterMeasure p) (f ⁻¹' s)
α : Type u_1
β : Type u_2
γ : Type ?u.44831
f : α → β
p : Pmf α
b : β
s : Set β
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ ↑↑(toMeasure (map f p)) s = ↑↑(toMeasure p) (f ⁻¹' s)
rw [toMeasure_apply_eq_toOuterMeasure_apply _ s hs,
  toMeasure_apply_eq_toOuterMeasure_apply _ (f ⁻¹' s) (measurableSet_preimage hf hs)]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.44831
f : α → β
p : Pmf α
b : β
s : Set β
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ ↑(toOuterMeasure (map f p)) s = ↑(toOuterMeasure p) (f ⁻¹' s)
exact toOuterMeasure_map_apply f p s