α : Type u_1
β : Type ?u.2377407
E : Type u_2
F : Type ?u.2377413
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : OpensMeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous f
a : α
⊢ IntegrableAtFilter f (𝓝[univ] a)
α : Type u_1
β : Type ?u.2377407
E : Type u_2
F : Type ?u.2377413
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : OpensMeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous f
a : α
⊢ IntegrableAtFilter f (𝓝 a)
rw [← nhdsWithin_univ]
no goals
α : Type u_1
β : Type ?u.2377407
E : Type u_2
F : Type ?u.2377413
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : OpensMeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Continuous f
a : α
⊢ IntegrableAtFilter f (𝓝[univ] a)
exact hf.continuousOn.integrableAt_nhdsWithin MeasurableSet.univ (mem_univ a)