English
Every standard Borel space is measurably equivalent to a subset of the real line.
Русский
Любое стандартное пространство Бореля измеримо эквивалентно подмножеству вещественных чисел.
LaTeX
$$$\exists s \subseteq \mathbb{R},\ MeasurableSet(s) \wedge \alpha \simeq^m s.$$$
Lean4
/-- Any standard Borel space is measurably equivalent to a subset of the reals. -/
theorem exists_subset_real_measurableEquiv : ∃ s : Set ℝ, MeasurableSet s ∧ Nonempty (α ≃ᵐ s) :=
by
by_cases hα : Countable α
· cases finite_or_infinite α
· obtain ⟨n, h_nonempty_equiv⟩ := exists_nat_measurableEquiv_range_coe_fin_of_finite α
refine ⟨_, ?_, h_nonempty_equiv⟩
letI : MeasurableSpace (Fin n) := borel (Fin n)
haveI : BorelSpace (Fin n) := ⟨rfl⟩
apply MeasurableEmbedding.measurableSet_range (mα := by infer_instance)
exact continuous_of_discreteTopology.measurableEmbedding (Nat.cast_injective.comp Fin.val_injective)
· refine ⟨_, ?_, measurableEquiv_range_coe_nat_of_infinite_of_countable α⟩
apply MeasurableEmbedding.measurableSet_range (mα := by infer_instance)
exact continuous_of_discreteTopology.measurableEmbedding Nat.cast_injective
· refine ⟨univ, MeasurableSet.univ, ⟨(PolishSpace.measurableEquivOfNotCountable hα ?_ : α ≃ᵐ (univ : Set ℝ))⟩⟩
rw [countable_coe_iff]
exact Cardinal.not_countable_real
