comp_aemeasurable — Mathlib

English

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

Русский

Если g является AЕ-измеримой относительно образа μ через f, и f — AЕ-измеримая относительно μ, то композиция g∘f является AЕ-измеримой относительно μ.

LaTeX

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

Lean4

theorem comp_aemeasurable {f : α → δ} {g : δ → β} (hg : AEMeasurable g (μ.map f)) (hf : AEMeasurable f μ) :
    AEMeasurable (g ∘ f) μ :=
  ⟨hg.mk g ∘ hf.mk f, hg.measurable_mk.comp hf.measurable_mk,
    (ae_eq_comp hf hg.ae_eq_mk).trans (hf.ae_eq_mk.fun_comp (mk g hg))⟩

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