measurable_ereal_toENNReal

Mathlib.MeasureTheory.Constructions.BorelSpace.Real

URI: https://scilib.ai/kg/mathlib#measurable_ereal_toENNReal

← MathLib Explorer

English

The map EReal → ENNReal sending x to its ENNReal value is measurable.

Русский

Отображение EReal → ENNReal, переводящее к значению ENNReal, измеримо.

LaTeX

$$$\\operatorname{Measurable}(\\mathrm{toENNReal}: \\mathrm{EReal} \\to \\mathrm{ENNReal})$$$

Lean4

@[measurability]
theorem measurable_ereal_toENNReal : Measurable EReal.toENNReal :=
  EReal.measurable_of_measurable_real (by simpa using ENNReal.measurable_ofReal)

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

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

Разделы

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

Аффилиация

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