Totally_Bounded_Metric_Space_is_Separable

import Mathlib.Topology.MetricSpace.Basic

theorem Totally_Bounded_Metric_Space_is_Separable {α : Type _} [PseudoMetricSpace α] (h : TotallyBounded (Set.univ : Set α)) : ∃ (s : Set α), s.Countable ∧ Dense s := by sorry