α : Type u_1
β : Type u_2
γ : Type ?u.309815
δ : Type ?u.309818
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ↑(Quotient.out' (mk f hf)) =ᵐ[μ] f
α : Type u_1
β : Type u_2
γ : Type ?u.309815
δ : Type ?u.309818
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ↑(mk f hf) =ᵐ[μ] f
apply (AEStronglyMeasurable.ae_eq_mk _).symm.trans
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.309815
δ : Type ?u.309818
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ↑(Quotient.out' (mk f hf)) =ᵐ[μ] f
exact @Quotient.mk_out' _ (μ.aeEqSetoid β) (⟨f, hf⟩ : { f // AEStronglyMeasurable f μ })