aemeasurable — Mathlib

English

Let f: X → Y be a continuous map between spaces equipped with appropriate σ-algebras; then f is ae-measurable with respect to any measure on X.

Русский

Пусть f: X → Y непрерывна между пространствами, снабжёнными соответствующими σ‑алгебрами; тогда f а.е.-измерима по любой мере на X.

LaTeX

$$$\\forall f:\\alpha\\to\\gamma\\,(Continuous(f)\\Rightarrow\\forall\\mu:\\mathrm{Measure}(\\alpha),\\ AEMeasurable(f,\\mu))$$$

Lean4

/-- A continuous function from an `OpensMeasurableSpace` to a `BorelSpace`
is ae-measurable. -/
@[fun_prop]
theorem aemeasurable {f : α → γ} (h : Continuous f) {μ : Measure α} : AEMeasurable f μ :=
  h.measurable.aemeasurable

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