ereal_toENNReal

Mathlib.MeasureTheory.Constructions.BorelSpace.Real

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

← MathLib Explorer

English

If f: α → EReal is measurable, then x ↦ (f(x)).toENNReal is measurable.

Русский

Если f: α → EReal измеримо, то x ↦ (f(x)).toENNReal измеримо.

LaTeX

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

Lean4

@[measurability, fun_prop]
theorem ereal_toENNReal {f : α → EReal} (hf : Measurable f) : Measurable fun x => (f x).toENNReal :=
  measurable_ereal_toENNReal.comp hf

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

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

Разделы

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

Аффилиация

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