coe_nnreal_ennreal — Mathlib

English

If f : α → NNReal is measurable, then x ↦ ENNReal.ofNNReal(f(x)) is measurable.

Русский

Если f: α → NNReal измерима, то x ↦ ENNReal.ofNNReal(f(x)) измеримо.

LaTeX

$$$\\\\forall f:\\\\alpha \\\\to \\\\mathbb{R}_{\\ge 0},\\\\;\\\\operatorname{Measurable}(f) \\\\Rightarrow \\\\operatorname{Measurable}(x \\\\mapsto \\\\operatorname{ENNReal}.ofNNReal(f(x))).$$$

Lean4

@[measurability, fun_prop]
theorem coe_nnreal_ennreal {f : α → ℝ≥0} (hf : Measurable f) : Measurable fun x => (f x : ℝ≥0∞) :=
  ENNReal.continuous_coe.measurable.comp hf

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