Theorems · Theorem · general topology

exists_nat_nat_continuous_surjective_of_completeSpace

∀ (α : Type u_2) [inst : MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [Nonempty α],
  ∃ f, Continuous f ∧ Function.Surjective f

Any nonempty complete second countable metric space is the continuous image of the fundamental space ℕ → ℕ. For a version of this theorem in the context of Polish spaces, see exists_nat_nat_continuous_surjective_of_polishSpace.

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

1 results in Mathlib

Foundations

Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MetricSpaceCompleteSpaceSecondCountableTopologyNonempty