real_toNNReal — Mathlib

English

If f: α → ℝ is measurable, then the function x ↦ Real.toNNReal(f(x)) is measurable.

Русский

Если f: α → ℝ измерима, то x ↦ Real.toNNReal(f(x)) измерима.

LaTeX

$$$\\\\text{Measurable}(f) \\\\Rightarrow \\\\text{Measurable}(x \\\\mapsto \\\\operatorname{Real.toNNReal}(f(x))).$$$

Lean4

@[measurability, fun_prop]
theorem real_toNNReal {f : α → ℝ} (hf : Measurable f) : Measurable fun x => Real.toNNReal (f x) :=
  measurable_real_toNNReal.comp hf

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