exists_measurableEmbedding_real — Mathlib

English

There exists a measurable embedding of any standard Borel space into the real numbers.

Русский

Существуют измеримые вложения любой стандартной борелевской пространства в множество вещественных чисел.

LaTeX

$$$\exists f:\alpha \to \mathbb{R},\ MeasurableEmbedding f.$$$

Lean4

/-- Any standard Borel space embeds measurably into the reals. -/
theorem exists_measurableEmbedding_real : ∃ f : α → ℝ, MeasurableEmbedding f :=
  by
  obtain ⟨s, hs, ⟨e⟩⟩ := exists_subset_real_measurableEquiv α
  exact ⟨(↑) ∘ e, (MeasurableEmbedding.subtype_coe hs).comp e.measurableEmbedding⟩

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