X : Type u_1
Y : Type ?u.129447
E : Type u_2
R : Type ?u.129453
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : TopologicalSpace Y
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s✝ : Set X
hf : LocallyIntegrable f
s : Set X
hs : MeasurableSet s
x : X
⊢ IntegrableAtFilter (Set.indicator s f) (𝓝 x)
X : Type u_1
Y : Type ?u.129447
E : Type u_2
R : Type ?u.129453
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : TopologicalSpace Y
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s✝ : Set X
hf : LocallyIntegrable f
s : Set X
hs : MeasurableSet s
⊢ LocallyIntegrable (Set.indicator s f)
intro x
case intro.intro
X : Type u_1
Y : Type ?u.129447
E : Type u_2
R : Type ?u.129453
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : TopologicalSpace Y
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s✝ : Set X
hf : LocallyIntegrable f
s : Set X
hs : MeasurableSet s
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : IntegrableOn f U
⊢ IntegrableAtFilter (Set.indicator s f) (𝓝 x)
X : Type u_1
Y : Type ?u.129447
E : Type u_2
R : Type ?u.129453
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : TopologicalSpace Y
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s✝ : Set X
hf : LocallyIntegrable f
s : Set X
hs : MeasurableSet s
x : X
⊢ IntegrableAtFilter (Set.indicator s f) (𝓝 x)
rcases hf x with ⟨U, hU, h'U⟩
no goals
case intro.intro
X : Type u_1
Y : Type ?u.129447
E : Type u_2
R : Type ?u.129453
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace Y
inst✝¹ : TopologicalSpace Y
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
s✝ : Set X
hf : LocallyIntegrable f
s : Set X
hs : MeasurableSet s
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : IntegrableOn f U
⊢ IntegrableAtFilter (Set.indicator s f) (𝓝 x)
exact ⟨U, hU, h'U.indicator hs⟩