measurableEmbedding_coe

Mathlib.MeasureTheory.Constructions.BorelSpace.Real

URI: https://scilib.ai/kg/mathlib#EReal.measurableEmbedding_coe

English

The embedding Real.toEReal is a measurable embedding.

Русский

Встраивание Real.toEReal является измеримым вложением.

LaTeX

$$$\\operatorname{MeasurableEmbedding}(\\mathrm{toEReal}: \\mathbb{R} \\to \\mathrm{EReal})$$$

Lean4

theorem measurableEmbedding_coe : MeasurableEmbedding Real.toEReal :=
  isOpenEmbedding_coe.measurableEmbedding

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

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

Разделы

Аффилиация

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