nnnorm — Mathlib

English

If f is measurable, then the function a ↦ SeminormedAddGroup.toNNNorm.nnnorm (f a) is measurable.

Русский

Если f измерима, то a ↦ SeminormedAddGroup.toNNNorm.nnnorm (f(a)) измеримо.

LaTeX

$$$\\text{Measurable}(f) \\Rightarrow \\text{Measurable}(\\lambda a. (\\text{SeminormedAddGroup.toNNNorm}).nnnorm (f(a)))$$$

Lean4

@[measurability, fun_prop]
protected theorem nnnorm {f : β → α} (hf : Measurable f) : Measurable fun a => ‖f a‖₊ :=
  measurable_nnnorm.comp hf

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