no goals
X : Type u_1
Y : Type ?u.127720
E : Type u_2
R : Type ?u.127726
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f
⊢ AEStronglyMeasurable f μ
simpa only [restrict_univ] using (locallyIntegrableOn_univ.mpr hf).aestronglyMeasurable