measurable_ereal_toReal

Mathlib.MeasureTheory.Constructions.BorelSpace.Real

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

English

The map EReal → ℝ that sends x to its real part is measurable.

Русский

Отображение EReal → ℝ, дающее вещественную часть, измеримо.

LaTeX

$$$\\operatorname{Measurable}(\\mathrm{toReal}: \\mathrm{EReal} \\to \\mathbb{R})$$$

Lean4

@[measurability]
theorem measurable_ereal_toReal : Measurable EReal.toReal :=
  EReal.measurable_of_measurable_real (by simpa using measurable_id)

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

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

Разделы

Аффилиация

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