α : Type u_1
β : Type u_2
γ : Type ?u.213751
δ : Type ?u.213754
ι : Type ?u.213757
R : Type ?u.213760
R' : Type ?u.213763
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f : α → β
hf : AEMeasurable f
⊢ ∀ (s : Set β), MeasurableSet s → ↑↑(map f μ) s = ↑(↑(OuterMeasure.map f) ↑μ) s
α : Type u_1
β : Type u_2
γ : Type ?u.213751
δ : Type ?u.213754
ι : Type ?u.213757
R : Type ?u.213760
R' : Type ?u.213763
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f : α → β
hf : AEMeasurable f
⊢ ↑(map f μ) = OuterMeasure.trim (↑(OuterMeasure.map f) ↑μ)
rw [← trimmed, OuterMeasure.trim_eq_trim_iff]
α : Type u_1
β : Type u_2
γ : Type ?u.213751
δ : Type ?u.213754
ι : Type ?u.213757
R : Type ?u.213760
R' : Type ?u.213763
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f : α → β
hf : AEMeasurable f
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f μ) s = ↑(↑(OuterMeasure.map f) ↑μ) s
α : Type u_1
β : Type u_2
γ : Type ?u.213751
δ : Type ?u.213754
ι : Type ?u.213757
R : Type ?u.213760
R' : Type ?u.213763
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f : α → β
hf : AEMeasurable f
⊢ ∀ (s : Set β), MeasurableSet s → ↑↑(map f μ) s = ↑(↑(OuterMeasure.map f) ↑μ) s
intro s hs
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.213751
δ : Type ?u.213754
ι : Type ?u.213757
R : Type ?u.213760
R' : Type ?u.213763
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f : α → β
hf : AEMeasurable f
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f μ) s = ↑(↑(OuterMeasure.map f) ↑μ) s
rw [map_apply_of_aemeasurable hf hs, OuterMeasure.map_apply]