α : Type u_1
β : Type u_2
γ : Type ?u.799057
δ : Type ?u.799060
ι : Type ?u.799063
R : Type ?u.799066
R' : Type ?u.799069
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
f : α ≃ᵐ β
h : SigmaFinite μ
⊢ SigmaFinite (Measure.map (↑(MeasurableEquiv.symm f)) (Measure.map (↑f) μ))
α : Type u_1
β : Type u_2
γ : Type ?u.799057
δ : Type ?u.799060
ι : Type ?u.799063
R : Type ?u.799066
R' : Type ?u.799069
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
f : α ≃ᵐ β
h : SigmaFinite μ
⊢ SigmaFinite (Measure.map (↑f) μ)
refine' SigmaFinite.of_map _ f.symm.measurable.aemeasurable _
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.799057
δ : Type ?u.799060
ι : Type ?u.799063
R : Type ?u.799066
R' : Type ?u.799069
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
f : α ≃ᵐ β
h : SigmaFinite μ
⊢ SigmaFinite (Measure.map (↑(MeasurableEquiv.symm f)) (Measure.map (↑f) μ))
rwa [map_map f.symm.measurable f.measurable, f.symm_comp_self, Measure.map_id]