mabs — Mathlib

English

If f is AEMeasurable, then x ↦ mabs(f(x)) is AEMeasurable (with respect to μ).

Русский

Если f является AEMeasurable, то x ↦ mabs(f(x)) является AEMeasurable по мере μ.

LaTeX

$$$\text{AEMeasurable}(f,\mu) \Rightarrow \text{AEMeasurable}\bigl(x \mapsto \mathrm{mabs}(f(x))\bigr)\,\mu$$$

Lean4

@[to_additive (attr := measurability, fun_prop)]
protected theorem mabs {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) : AEMeasurable (fun x ↦ mabs (f x)) μ :=
  measurable_mabs.comp_aemeasurable hf

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