Theorem: MeasureTheory.map_measureReal_apply (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (map f μ).real s = μ.real (f ⁻¹' s)
Tactic:
rw [measureReal_def, map_apply hf hs]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (μ (f ⁻¹' s)).toReal = μ.real (f ⁻¹' s)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (μ (f ⁻¹' s)).toReal = μ.real (f ⁻¹' s)
Tactic:
rfl
State after:
no goals