measurable_coe_ennreal_comp — Mathlib

English

For an open-measurable space X, the composition of a bounded continuous function with the Ennreal coercion is measurable.

Русский

Для пространства X с открытым измеримостным пространством композиция ограниченной непрерывной функции с преобразованием к Ennreal измерима.

LaTeX

$$$$\\text{Measurable}\\left( x \\mapsto (f(x) : \\mathbb{R}_{\\ge 0}^{\\infty})\\right).$$$$

Lean4

theorem measurable_coe_ennreal_comp [OpensMeasurableSpace X] (f : X →ᵇ ℝ≥0) : Measurable fun x ↦ (f x : ℝ≥0∞) :=
  measurable_coe_nnreal_ennreal.comp f.continuous.measurable

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