measurableEquivNatBoolOfNotCountable

English

There exists a measurable equivalence between uncountable standard Borel spaces and Cantor-like spaces (Nat → Bool).

Русский

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

LaTeX

$$MeasurableEquiv α (Nat → Bool)$$

Lean4

/-- Any uncountable standard Borel space is Borel isomorphic to the Cantor space `ℕ → Bool`. -/
noncomputable def measurableEquivNatBoolOfNotCountable (h : ¬Countable α) : α ≃ᵐ (ℕ → Bool) :=
  by
  apply Nonempty.some
  letI := upgradeStandardBorel α
  obtain ⟨f, -, fcts, finj⟩ :=
    isClosed_univ.exists_nat_bool_injection_of_not_countable (α := α)
      (by rwa [← countable_coe_iff, (Equiv.Set.univ _).countable_iff])
  obtain ⟨g, gmeas, ginj⟩ := MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated α
  exact ⟨borelSchroederBernstein gmeas ginj fcts.measurable finj⟩

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