X : Type u_1
Y : Type ?u.711872
E : Type u_2
R : Type ?u.711878
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : NormedAddCommGroup E
f : X → E
μ : MeasureTheory.Measure X
s : Set X
inst✝² : OpensMeasurableSpace X
inst✝¹ : IsLocallyFiniteMeasure μ
K : Set X
a b : X
inst✝ : MetrizableSpace X
hK : IsCompact K
hf : ContinuousOn f K
this : MetricSpace X := metrizableSpaceMetric X
⊢ IntegrableOn f K
X : Type u_1
Y : Type ?u.711872
E : Type u_2
R : Type ?u.711878
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : NormedAddCommGroup E
f : X → E
μ : MeasureTheory.Measure X
s : Set X
inst✝² : OpensMeasurableSpace X
inst✝¹ : IsLocallyFiniteMeasure μ
K : Set X
a b : X
inst✝ : MetrizableSpace X
hK : IsCompact K
hf : ContinuousOn f K
⊢ IntegrableOn f K
letI := metrizableSpaceMetric X
X : Type u_1
Y : Type ?u.711872
E : Type u_2
R : Type ?u.711878
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : NormedAddCommGroup E
f : X → E
μ : MeasureTheory.Measure X
s : Set X
inst✝² : OpensMeasurableSpace X
inst✝¹ : IsLocallyFiniteMeasure μ
K : Set X
a b : X
inst✝ : MetrizableSpace X
hK : IsCompact K
hf : ContinuousOn f K
this : MetricSpace X := metrizableSpaceMetric X
x : X
hx : x ∈ K
⊢ IntegrableAtFilter f (𝓝[K] x)
X : Type u_1
Y : Type ?u.711872
E : Type u_2
R : Type ?u.711878
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : NormedAddCommGroup E
f : X → E
μ : MeasureTheory.Measure X
s : Set X
inst✝² : OpensMeasurableSpace X
inst✝¹ : IsLocallyFiniteMeasure μ
K : Set X
a b : X
inst✝ : MetrizableSpace X
hK : IsCompact K
hf : ContinuousOn f K
this : MetricSpace X := metrizableSpaceMetric X
⊢ IntegrableOn f K
refine' LocallyIntegrableOn.integrableOn_isCompact (fun x hx => _) hK
no goals
X : Type u_1
Y : Type ?u.711872
E : Type u_2
R : Type ?u.711878
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : NormedAddCommGroup E
f : X → E
μ : MeasureTheory.Measure X
s : Set X
inst✝² : OpensMeasurableSpace X
inst✝¹ : IsLocallyFiniteMeasure μ
K : Set X
a b : X
inst✝ : MetrizableSpace X
hK : IsCompact K
hf : ContinuousOn f K
this : MetricSpace X := metrizableSpaceMetric X
x : X
hx : x ∈ K
⊢ IntegrableAtFilter f (𝓝[K] x)
exact hf.integrableAt_nhdsWithin_of_isSeparable hK.measurableSet hK.isSeparable hx