A Polish Borel space is measurably equivalent to a set of reals

theorem MeasureTheory.exists_nat_measurableEquiv_range_coe_fin_of_finite (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] [Finite α] : ∃ (n : ℕ), Nonempty (α ≃ᵐ ↑(Set.range fun (x : Fin n) => ↑↑x))

theorem MeasureTheory.measurableEquiv_range_natCast_of_infinite_of_countable (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] [Infinite α] [Countable α] : Nonempty (α ≃ᵐ ↑(Set.range Nat.cast))

@[deprecated MeasureTheory.measurableEquiv_range_natCast_of_infinite_of_countable (since := "2026-10-13")]

theorem MeasureTheory.measurableEquiv_range_coe_nat_of_infinite_of_countable (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] [Infinite α] [Countable α] : Nonempty (α ≃ᵐ ↑(Set.range Nat.cast))

Alias of MeasureTheory.measurableEquiv_range_natCast_of_infinite_of_countable.

theorem MeasureTheory.exists_subset_real_measurableEquiv (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] : ∃ (s : Set ℝ), MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)

Any standard Borel space is measurably equivalent to a subset of the reals.

theorem MeasureTheory.exists_measurableEmbedding_real (α : Type u_1) [MeasurableSpace α] [StandardBorelSpace α] : ∃ (f : α → ℝ), MeasurableEmbedding f

Any standard Borel space embeds measurably into the reals.

noncomputable def MeasureTheory.embeddingReal (Ω : Type u_2) [MeasurableSpace Ω] [StandardBorelSpace Ω] : Ω → ℝ

A measurable embedding of a standard Borel space into ℝ.

Equations

• MeasureTheory.embeddingReal Ω = ⋯.choose

theorem MeasureTheory.measurableEmbedding_embeddingReal (Ω : Type u_2) [MeasurableSpace Ω] [StandardBorelSpace Ω] : MeasurableEmbedding (embeddingReal Ω)

theorem MeasureTheory.measurable_embeddingReal (Ω : Type u_2) [MeasurableSpace Ω] [StandardBorelSpace Ω] : Measurable (embeddingReal Ω)