measurableEquiv_range_coe_nat_of_infinite_of_countable

English

Let α be an infinite countable type. Then there exists a measurable equivalence between α and the range of the natural embedding of ℕ into ℝ.

Русский

Пусть α бесконечно счётно. Существует измеримая эквивалентность между α и диапазоном отображения ℕ в ℝ.

LaTeX

$$$\exists \phi:\alpha \overset{\mathrm{m}}{\simeq} \mathrm{range}(\mathrm{Nat.cast}: \mathbb{N} \to \mathbb{R}).$$$

Lean4

theorem measurableEquiv_range_coe_nat_of_infinite_of_countable [Infinite α] [Countable α] :
    Nonempty (α ≃ᵐ range ((↑) : ℕ → ℝ)) :=
  by
  have : PolishSpace (range ((↑) : ℕ → ℝ)) := Nat.isClosedEmbedding_coe_real.isClosedMap.isClosed_range.polishSpace
  refine ⟨PolishSpace.Equiv.measurableEquiv ?_⟩
  refine (nonempty_equiv_of_countable.some : α ≃ ℕ).trans ?_
  exact Equiv.ofInjective ((↑) : ℕ → ℝ) Nat.cast_injective

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