comp_aemeasurable' — Mathlib

English

The primed version asserts the same composition rule in a slightly different form: g ∘ f is AEMeasurable when hg is measurable and hf is AEMeasurable.

Русский

Уточненная версия утверждает ту же самую формулу композиции: AEMeasurable(g∘f) когда hg измерима, hf AEMeasurable.

LaTeX

$$$\text{Measurable}(g) \rightarrow \mathrm{AEMeasurable}(f)\mu \rightarrow \mathrm{AEMeasurable}(\lambda x. g(f(x)))\mu$$$

Lean4

@[fun_prop, measurability]
theorem comp_aemeasurable' [MeasurableSpace δ] {f : α → δ} {g : δ → β} (hg : Measurable g) (hf : AEMeasurable f μ) :
    AEMeasurable (fun x ↦ g (f x)) μ :=
  Measurable.comp_aemeasurable hg hf

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