measurable_coe_real_ereal

Mathlib.MeasureTheory.Constructions.BorelSpace.Real

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

English

The canonical inclusion i: R → EReal is a measurable map.

Русский

Каноническое вложение i: ℝ → EReal является измеримым отображением.

LaTeX

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

Lean4

@[measurability, fun_prop]
theorem measurable_coe_real_ereal : Measurable ((↑) : ℝ → EReal) :=
  continuous_coe_real_ereal.measurable

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

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

Разделы

Аффилиация

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