comp_nullMeasurable — Mathlib

English

If g is measurable and f is null-measurable with respect to μ, then the composition g ∘ f is null-measurable with respect to μ.

Русский

Если g измеримa, а f — нулевой измеримa относитeльно μ, тогда композиция g ∘ f является нулевой измеримостью по μ.

LaTeX

$$$\mathrm{Measurable}(g) \wedge \mathrm{NullMeasurable}(f,\mu) \Rightarrow \mathrm{NullMeasurable}(g\circ f,\mu).$$$

Lean4

theorem comp_nullMeasurable {g : β → γ} (hg : Measurable g) (hf : NullMeasurable f μ) : NullMeasurable (g ∘ f) μ :=
  hg.comp_eventuallyMeasurable hf

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