X : Type u_1
Y : Type ?u.121628
E : Type u_2
R : Type ?u.121634
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : TopologicalSpace Y
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
⊢ (∀ (x : X), IntegrableAtFilter f (𝓝 x)) ↔ LocallyIntegrable f
X : Type u_1
Y : Type ?u.121628
E : Type u_2
R : Type ?u.121634
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : TopologicalSpace Y
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
⊢ LocallyIntegrableOn f univ ↔ LocallyIntegrable f
simp only [LocallyIntegrableOn, nhdsWithin_univ, mem_univ, true_imp_iff]
no goals
X : Type u_1
Y : Type ?u.121628
E : Type u_2
R : Type ?u.121634
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : TopologicalSpace Y
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
⊢ (∀ (x : X), IntegrableAtFilter f (𝓝 x)) ↔ LocallyIntegrable f
rfl