English
If f is continuous on a compact set s, then f is AEStronglyMeasurable with respect to μ.restrict s.
Русский
Если f непрерывна на компактном множестве s, то f является AEStronglyMeasurable относительно μ.restrict s.
LaTeX
$$$\\text{AEStronglyMeasurable } f (\\mu \\restriction s)$$$
Lean4
/-- If a function is continuous on an open set `s`, then it is strongly measurable at the filter
`𝓝 x` for all `x ∈ s` if either the source space or the target space is second-countable. -/
theorem stronglyMeasurableAtFilter [TopologicalSpace α] [OpensMeasurableSpace α] [TopologicalSpace β]
[PseudoMetrizableSpace β] [SecondCountableTopologyEither α β] {f : α → β} {s : Set α} {μ : Measure α}
(hs : IsOpen s) (hf : ContinuousOn f s) : ∀ x ∈ s, StronglyMeasurableAtFilter f (𝓝 x) μ := fun _x hx =>
⟨s, IsOpen.mem_nhds hs hx, hf.aestronglyMeasurable hs.measurableSet⟩
