English
If a function is continuous on a set t, second-countable, and a ∈ t, then f is integrable at nhdsWithin a t.
Русский
Если функция непрерывна на t и t обладает счетной базой, и a ∈ t, то f интегрируема в nhdsWithin a t.
LaTeX
$$$\\text{IntegrableAtFilter } f (\\nhdsWithin a t) μ$ under appropriate second countability assumptions.$$
Lean4
theorem integrableAt_nhdsWithin [TopologicalSpace α] [SecondCountableTopologyEither α E] [OpensMeasurableSpace α]
{μ : Measure α} [IsLocallyFiniteMeasure μ] {a : α} {t : Set α} {f : α → E} (hft : ContinuousOn f t)
(ht : MeasurableSet t) (ha : a ∈ t) : IntegrableAtFilter f (𝓝[t] a) μ :=
haveI : (𝓝[t] a).IsMeasurablyGenerated := ht.nhdsWithin_isMeasurablyGenerated _
(hft a ha).integrableAtFilter ⟨_, self_mem_nhdsWithin, hft.aestronglyMeasurable ht⟩ (μ.finiteAt_nhdsWithin _ _)
