comp_aemeasurable — Mathlib

English

If g is measurable and f is AEMeasurable, then g ∘ f is AEMeasurable.

Русский

Если g измерима, а f AEMеасимируемо, то композиция g ∘ f является AEMеасимируемой.

LaTeX

$$$\text{Measurable}(g) \rightarrow \mathrm{AEMeasurable}(f) \mu \rightarrow \mathrm{AEMeasurable}(g\circ f)\mu$$$

Lean4

theorem comp_aemeasurable [MeasurableSpace δ] {f : α → δ} {g : δ → β} (hg : Measurable g) (hf : AEMeasurable f μ) :
    AEMeasurable (g ∘ f) μ :=
  ⟨g ∘ hf.mk f, hg.comp hf.measurable_mk, EventuallyEq.fun_comp hf.ae_eq_mk _⟩

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