comp_measurable — Mathlib

English

If g is AEMeasurable with μ.map f and f is Measurable, then g∘f is AEMeasurable with μ.

Русский

Если g — AЕ-измеримая относительно μ.map f, а f — измеримая, то g∘f — AЕ-измеримая относительно μ.

LaTeX

$$$\mathrm{AEMeasurable}(g \circ f, \mu) \leftarrow \mathrm{AEMeasurable}(g, \mu\map f) \rightarrow \mathrm{Measurable}(f) \rightarrow \mathrm{AEMeasurable}(g \circ f, \mu)$$$

Lean4

theorem comp_measurable {f : α → δ} {g : δ → β} (hg : AEMeasurable g (μ.map f)) (hf : Measurable f) :
    AEMeasurable (g ∘ f) μ :=
  hg.comp_aemeasurable hf.aemeasurable

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