measurableEmbedding_embeddingReal

English

For any Ω with a measurable space, there is a measurable embedding of the measurable space into the reals.

Русский

Для любого Ω с измеряемым пространством существует измеримое вложение в вещественные числа.

LaTeX

$$$\exists \text{ embeddingReal}: \Omega \to \mathbb{R},\ MeasurableEmbedding(embeddingReal \Omega).$$$

Lean4

theorem measurableEmbedding_embeddingReal (Ω : Type*) [MeasurableSpace Ω] [StandardBorelSpace Ω] :
    MeasurableEmbedding (embeddingReal Ω) :=
  (exists_measurableEmbedding_real Ω).choose_spec

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