measurable_coe_ennreal_ereal

Mathlib.MeasureTheory.Constructions.BorelSpace.Real

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

English

The embedding ℝ≥0∞ → EReal given by coercion is measurable.

Русский

Встраивание ℝ≥0∞ в EReal по включению измеримо.

LaTeX

$$$\\operatorname{Measurable}((\\uparrow): \\mathbb{R}_{\ge 0}^{\\infty} \\to \\mathrm{EReal})$$$

Lean4

@[measurability]
theorem measurable_coe_ennreal_ereal : Measurable ((↑) : ℝ≥0∞ → EReal) :=
  continuous_coe_ennreal_ereal.measurable

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

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

Разделы

Аффилиация

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