real_toNNReal — Mathlib

English

If f is AEStronglyMeasurable, then the real-valued toNNReal version is AEStronglyMeasurable.

Русский

Если f реального типа, то его toNNReal-образ является AEStronglyMeasurable.

LaTeX

$$$AEStronglyMeasurable(f, \mu) \Rightarrow AEStronglyMeasurable(([f(x)].toNNReal), \mu)$$$

Lean4

@[fun_prop, measurability]
protected theorem real_toNNReal {f : α → ℝ} (hf : AEStronglyMeasurable f μ) :
    AEStronglyMeasurable (fun x => (f x).toNNReal) μ :=
  continuous_real_toNNReal.comp_aestronglyMeasurable hf

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