real_toNNReal — Mathlib

English

The enorm (enormous norm) of a strongly measurable function is measurable.

Русский

enorm (норма) сильно измеримой функции — измеримо.

LaTeX

$$$\mathrm{Measurable}(\|f\|_{\mathbb{e}}) \text{ for } f \text{ strongly measurable}$$$

Lean4

@[fun_prop, measurability]
protected theorem real_toNNReal {_ : MeasurableSpace α} {f : α → ℝ} (hf : StronglyMeasurable f) :
    StronglyMeasurable fun x => (f x).toNNReal :=
  continuous_real_toNNReal.comp_stronglyMeasurable hf

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