case a
α : Type u_1
β : Type u_2
γ : Type ?u.2927971
δ : Type ?u.2927974
ι : Type ?u.2927977
R : Type ?u.2927980
R' : Type ?u.2927983
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
f : α ≃ᵐ β
μ : MeasureTheory.Measure α
s : Set β
⊢ s ∈ Filter.map (↑f) (ae μ) ↔ s ∈ ae (Measure.map (↑f) μ)
α : Type u_1
β : Type u_2
γ : Type ?u.2927971
δ : Type ?u.2927974
ι : Type ?u.2927977
R : Type ?u.2927980
R' : Type ?u.2927983
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
f : α ≃ᵐ β
μ : MeasureTheory.Measure α
⊢ Filter.map (↑f) (ae μ) = ae (Measure.map (↑f) μ)
ext s
no goals
case a
α : Type u_1
β : Type u_2
γ : Type ?u.2927971
δ : Type ?u.2927974
ι : Type ?u.2927977
R : Type ?u.2927980
R' : Type ?u.2927983
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
f : α ≃ᵐ β
μ : MeasureTheory.Measure α
s : Set β
⊢ s ∈ Filter.map (↑f) (ae μ) ↔ s ∈ ae (Measure.map (↑f) μ)
simp_rw [mem_map, mem_ae_iff, ← preimage_compl, f.map_apply]