ennreal_toNNReal

Mathlib.MeasureTheory.Constructions.BorelSpace.Real

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

← MathLib Explorer

English

A limit (over a general filter) of a.e.-measurable ENNReal-valued functions is a.e.-measurable.

Русский

Предел a.e.-измеримых функций ENNReal по общему фильтру — тоже a.e.-измерим.

LaTeX

$$$\text{aemeasurable_of_tendsto}$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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