ennreal_toReal

Mathlib.MeasureTheory.Constructions.BorelSpace.Real

URI: https://scilib.ai/kg/mathlib#Measurable.ennreal_toReal

← MathLib Explorer

English

If f is measurable, then its real-valued transformation toReal(f) is measurable.

Русский

Если функция измерима, то её преобразование toReal(f) измеримо.

LaTeX

$$$\text{Measurable}(f) \Rightarrow \text{Measurable}(\text{toReal}(f))$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru