exists_nat_nat_continuous_surjective

English

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

Русский

То же самое, что и в 207045.

LaTeX

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

Lean4

/-- Any nonempty Polish space is the continuous image of the fundamental space `ℕ → ℕ`. -/
theorem exists_nat_nat_continuous_surjective (α : Type*) [TopologicalSpace α] [PolishSpace α] [Nonempty α] :
    ∃ f : (ℕ → ℕ) → α, Continuous f ∧ Surjective f :=
  letI := upgradeIsCompletelyMetrizable α
  exists_nat_nat_continuous_surjective_of_completeSpace α

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