stronglyMeasurableAtFilter — Mathlib

English

A continuous function on a set has strong measurability at every point with respect to the ambient measure.

Русский

Непрерывная функция на множестве имеет сильную измеримость в точке по исходной мере.

LaTeX

$$$\\text{StronglyMeasurableAtFilter } f (\\mathcal{N} x) μ$ for all x when f is continuous.$$

Lean4

theorem stronglyMeasurableAtFilter [TopologicalSpace α] [OpensMeasurableSpace α] [TopologicalSpace β]
    [PseudoMetrizableSpace β] [SecondCountableTopologyEither α β] {f : α → β} (hf : Continuous f) (μ : Measure α)
    (l : Filter α) : StronglyMeasurableAtFilter f l μ :=
  hf.stronglyMeasurable.stronglyMeasurableAtFilter

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