nnnorm — Mathlib

English

If f is AEStronglyMeasurable, then the nonnegative-norm map x ↦ ‖f(x)‖₊ is AEStronglyMeasurable.

Русский

Если f является AEStronglyMeasurable, то ‖f(x)‖₊ является AEStronglyMeasurable.

LaTeX

$$$AEStronglyMeasurable(f, \mu) \Rightarrow AEStronglyMeasurable(\lambda x. \|f(x)\|_+, \mu)$$$

Lean4

@[fun_prop, measurability]
protected theorem nnnorm {β : Type*} [SeminormedAddCommGroup β] {f : α → β} (hf : AEStronglyMeasurable f μ) :
    AEStronglyMeasurable (fun x => ‖f x‖₊) μ :=
  continuous_nnnorm.comp_aestronglyMeasurable hf

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