Theorems · Theorem · general topology

TotallyBounded.isSeparable

∀ {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] {s : Set α},
  TotallyBounded s → TopologicalSpace.IsSeparable s

A totally bounded set is separable in countably generated uniform spaces. This can be obtained from the more general UniformSpace.subset_countable_closure_of_almost_dense_set.

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpaceFilter.IsCountablyGenerated