α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.407802
ι : Type ?u.407805
R : Type ?u.407808
R' : Type ?u.407811
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g
hf : QuasiMeasurePreserving f
⊢ map g (map f μa) ≪ μc
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.407802
ι : Type ?u.407805
R : Type ?u.407808
R' : Type ?u.407811
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g
hf : QuasiMeasurePreserving f
⊢ map (g ∘ f) μa ≪ μc
rw [← map_map hg.1 hf.1]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.407802
ι : Type ?u.407805
R : Type ?u.407808
R' : Type ?u.407811
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f✝ : α → β
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g
hf : QuasiMeasurePreserving f
⊢ map g (map f μa) ≪ μc
exact (hf.2.map hg.1).trans hg.2