X : Type u_1
Y : Type ?u.122795
E : Type u_2
R : Type ?u.122801
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f
x : X
a✝ : x ∈ s
⊢ IntegrableAtFilter f (𝓝[s] x)
X : Type u_1
Y : Type ?u.122795
E : Type u_2
R : Type ?u.122801
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f
⊢ LocallyIntegrableOn f s
intro x _
case intro.intro
X : Type u_1
Y : Type ?u.122795
E : Type u_2
R : Type ?u.122801
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f
x : X
a✝ : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t
⊢ IntegrableAtFilter f (𝓝[s] x)
X : Type u_1
Y : Type ?u.122795
E : Type u_2
R : Type ?u.122801
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f
x : X
a✝ : x ∈ s
⊢ IntegrableAtFilter f (𝓝[s] x)
obtain ⟨t, ht_mem, ht_int⟩ := hf x
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.122795
E : Type u_2
R : Type ?u.122801
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f
x : X
a✝ : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t
u : Set X
hu_sub : u ⊆ t
hu_o : IsOpen u
hu_mem : x ∈ u
⊢ IntegrableAtFilter f (𝓝[s] x)
case intro.intro
X : Type u_1
Y : Type ?u.122795
E : Type u_2
R : Type ?u.122801
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f
x : X
a✝ : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t
⊢ IntegrableAtFilter f (𝓝[s] x)
obtain ⟨u, hu_sub, hu_o, hu_mem⟩ := mem_nhds_iff.mp ht_mem
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.122795
E : Type u_2
R : Type ?u.122801
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f
x : X
a✝ : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t
u : Set X
hu_sub : u ⊆ t
hu_o : IsOpen u
hu_mem : x ∈ u
⊢ IntegrableOn f (s ∩ u)
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.122795
E : Type u_2
R : Type ?u.122801
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f
x : X
a✝ : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t
u : Set X
hu_sub : u ⊆ t
hu_o : IsOpen u
hu_mem : x ∈ u
⊢ IntegrableAtFilter f (𝓝[s] x)
refine' ⟨_, inter_mem_nhdsWithin s (hu_o.mem_nhds hu_mem), _⟩
no goals
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type ?u.122795
E : Type u_2
R : Type ?u.122801
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace Y
inst✝² : TopologicalSpace Y
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f
x : X
a✝ : x ∈ s
t : Set X
ht_mem : t ∈ 𝓝 x
ht_int : IntegrableOn f t
u : Set X
hu_sub : u ⊆ t
hu_o : IsOpen u
hu_mem : x ∈ u
⊢ IntegrableOn f (s ∩ u)
simpa only [IntegrableOn, Measure.restrict_restrict hu_o.measurableSet, inter_comm] using
  ht_int.mono_set hu_sub