polishSpace_induced — Mathlib

English

Same as 207045: every nonempty complete second-countable metric space is the continuous image of ℕ→ℕ.

Русский

То же самое: каждое непустое полное метрическое пространство со счетным базисом – непрерывное изображение ℕ→ℕ.

LaTeX

$$$$\\\\exists f:(\\\\mathbb{N}\\\\rightarrow\\\\mathbb{N})\\\\rightarrow α, \\\\text{Continuous } f \\\\land \\\\text{Surjective } f.$$$$

Lean4

/-- Pulling back a Polish topology under an equiv gives again a Polish topology. -/
theorem _root_.Equiv.polishSpace_induced [t : TopologicalSpace β] [PolishSpace β] (f : α ≃ β) :
    @PolishSpace α (t.induced f) :=
  letI : TopologicalSpace α := t.induced f
  (f.toHomeomorphOfIsInducing ⟨rfl⟩).isClosedEmbedding.polishSpace

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