X : Type u_1
Y : Type ?u.128412
E : Type u_2
R : Type ?u.128418
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : IsLocallyFiniteMeasure μ
c : E
x : X
⊢ IntegrableAtFilter (fun x => c) (𝓝 x)
X : Type u_1
Y : Type ?u.128412
E : Type u_2
R : Type ?u.128418
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : IsLocallyFiniteMeasure μ
c : E
⊢ LocallyIntegrable fun x => c
intro x
case intro.intro
X : Type u_1
Y : Type ?u.128412
E : Type u_2
R : Type ?u.128418
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : IsLocallyFiniteMeasure μ
c : E
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : ↑↑μ U < ⊤
⊢ IntegrableAtFilter (fun x => c) (𝓝 x)
X : Type u_1
Y : Type ?u.128412
E : Type u_2
R : Type ?u.128418
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : IsLocallyFiniteMeasure μ
c : E
x : X
⊢ IntegrableAtFilter (fun x => c) (𝓝 x)
rcases μ.finiteAt_nhds x with ⟨U, hU, h'U⟩
case intro.intro
X : Type u_1
Y : Type ?u.128412
E : Type u_2
R : Type ?u.128418
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : IsLocallyFiniteMeasure μ
c : E
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : ↑↑μ U < ⊤
⊢ IntegrableOn (fun x => c) U
case intro.intro
X : Type u_1
Y : Type ?u.128412
E : Type u_2
R : Type ?u.128418
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : IsLocallyFiniteMeasure μ
c : E
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : ↑↑μ U < ⊤
⊢ IntegrableAtFilter (fun x => c) (𝓝 x)
refine' ⟨U, hU, _⟩
no goals
case intro.intro
X : Type u_1
Y : Type ?u.128412
E : Type u_2
R : Type ?u.128418
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : IsLocallyFiniteMeasure μ
c : E
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : ↑↑μ U < ⊤
⊢ IntegrableOn (fun x => c) U
simp only [h'U, integrableOn_const, or_true_iff]