real_toNNReal — Mathlib

English

If f is almost everywhere measurable with respect to μ, then x ↦ Real.toNNReal(f(x)) is also almost everywhere measurable with respect to μ.

Русский

Если f измеримо почти повсеместно относительно μ, то x ↦ Real.toNNReal(f(x)) тоже измеримо почти повсеместно относительно μ.

LaTeX

$$$\\\\text{AEMeasurable}(f,\\\\mu) \\\\Rightarrow \\\\text{AEMeasurable}(x \\\\mapsto \\\\operatorname{Real.toNNReal}(f(x))).$$$

Lean4

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

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