Theorems · Theorem · general topology

DenseRange.separableSpace

∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [inst : TopologicalSpace β]
  {f : α → β}, DenseRange f → Continuous f → TopologicalSpace.SeparableSpace β

If α is a separable space and f : α → β is a continuous map with dense range, then β is a separable space as well. E.g., the completion of a separable uniform space is separable.

Defined in

Mathlib.Topology.Bases

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace.SeparableSpaceTopologicalSpace