measurable_coe_nnreal_ennreal — Mathlib

English

If f is measurable, then the map from NNReal to ENNReal given by ENNReal.continuous_coe is measurable.

Русский

Если f измерим, то переход от NNReal к ENNReal по включению измерим.

LaTeX

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

Lean4

@[measurability]
theorem measurable_coe_nnreal_ennreal : Measurable ((↑) : ℝ≥0 → ℝ≥0∞) :=
  ENNReal.continuous_coe.measurable

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