α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.350267
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
hg : Continuous g
f : α →ₘ[μ] β
⊢ ↑(mk (g ∘ ↑f) (_ : AEStronglyMeasurable (fun x => g (↑f x)) μ)) =ᵐ[μ] g ∘ ↑f
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.350267
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
hg : Continuous g
f : α →ₘ[μ] β
⊢ ↑(comp g hg f) =ᵐ[μ] g ∘ ↑f
rw [comp_eq_mk]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.350267
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
hg : Continuous g
f : α →ₘ[μ] β
⊢ ↑(mk (g ∘ ↑f) (_ : AEStronglyMeasurable (fun x => g (↑f x)) μ)) =ᵐ[μ] g ∘ ↑f
apply coeFn_mk