comp_aemeasurable' — Mathlib

English

A variant: AEMeasurable g ∘ f from AEMeasurable g ∘ f μ is equivalent to the same with f and g in the given form.

Русский

Вариант: AЕ-измеримость композиции g∘f имеет такую же форму утверждения в данном виде.

LaTeX

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

Lean4

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

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