stronglyMeasurableAtFilter_nhdsWithin

English

If f is continuous on a measurable set s, then f is measurable at nhdsWithin x s for any x.

Русский

Если f непрерывна на измеримом множестве s, то f измерима в окрестности nhdsWithin x s для любого x.

LaTeX

$$$\\text{StronglyMeasurableAtFilter } f (\\mathcal{N}[s] x) μ$ for all x.$$

Lean4

/-- If a function is continuous on a measurable set `s`, then it is measurable at the filter
  `𝓝[s] x` for all `x`. -/
theorem stronglyMeasurableAtFilter_nhdsWithin {α β : Type*} [MeasurableSpace α] [TopologicalSpace α]
    [OpensMeasurableSpace α] [TopologicalSpace β] [PseudoMetrizableSpace β] [SecondCountableTopologyEither α β]
    {f : α → β} {s : Set α} {μ : Measure α} (hf : ContinuousOn f s) (hs : MeasurableSet s) (x : α) :
    StronglyMeasurableAtFilter f (𝓝[s] x) μ :=
  ⟨s, self_mem_nhdsWithin, hf.aestronglyMeasurable hs⟩

Похожие утверждения