measurable_ofReal

Mathlib.MeasureTheory.Constructions.BorelSpace.Real

URI: https://scilib.ai/kg/mathlib#ENNReal.measurable_ofReal

English

The map ENNReal.ofReal is measurable.

Русский

Очередная функция ENNReal.ofReal измерима.

LaTeX

$$$\operatorname{Measurable}(\,\text{ENNReal.ofReal}\,)$$$

Lean4

@[measurability]
theorem measurable_ofReal : Measurable ENNReal.ofReal :=
  ENNReal.continuous_ofReal.measurable

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

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

Разделы

Аффилиация

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