measurable_embeddingReal

Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measurable_embeddingReal

← MathLib Explorer

English

The embeddingReal function is measurable.

Русский

Функция embeddingReal измерима.

LaTeX

$$$\text{MeasurableEmbedding}(\text{embeddingReal} \Omega)$ is a measurable embedding.$$

Lean4

@[fun_prop]
theorem measurable_embeddingReal (Ω : Type*) [MeasurableSpace Ω] [StandardBorelSpace Ω] :
    Measurable (embeddingReal Ω) :=
  (measurableEmbedding_embeddingReal Ω).measurable

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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