stronglyMeasurableAtFilter — Mathlib

English

If s is open and f is continuous on s, then f is strongly measurable at nhds x for every x ∈ s.

Русский

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

LaTeX

$$$\\forall x\\in s,\\; StronglyMeasurableAtFilter f (\\mathcal{N} x) μ$$$

Lean4

theorem stronglyMeasurableAtFilter [TopologicalSpace α] [OpensMeasurableSpace α] [SecondCountableTopologyEither α E]
    {f : α → E} {s : Set α} {μ : Measure α} (hs : IsOpen s) (hf : ∀ x ∈ s, ContinuousAt f x) :
    ∀ x ∈ s, StronglyMeasurableAtFilter f (𝓝 x) μ :=
  ContinuousOn.stronglyMeasurableAtFilter hs <| continuousOn_of_forall_continuousAt hf

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