English
A totally bounded set is separable in a countably generated uniform space.
Русский
Totally bounded множество в счетно порождаемом равномерном пространстве сепарируемо.
LaTeX
$$$[UniformSpace X] [IsCountablyGenerated (\\mathcal U X)] {s : Set X}\\; (h : TotallyBounded s)\\Rightarrow TopologicalSpace.IsSeparable s$$$
Lean4
/-- A totally bounded set is separable in countably generated uniform spaces. This can be obtained
from the more general `EMetric.subset_countable_closure_of_almost_dense_set`. -/
theorem isSeparable [UniformSpace X] [i : IsCountablyGenerated (𝓤 X)] {s : Set X} (h : TotallyBounded s) :
TopologicalSpace.IsSeparable s :=
by
letI := (UniformSpace.pseudoMetricSpace (X := X)).toPseudoEMetricSpace
rw [EMetric.totallyBounded_iff] at h
have h' : ∀ ε > 0, ∃ t, Set.Countable t ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε :=
by
intro ε hε
obtain ⟨t, ht⟩ := h ε hε
refine ⟨t, ht.1.countable, subset_trans ht.2 ?_⟩
gcongr
exact EMetric.ball_subset_closedBall
obtain ⟨t, _, htc, hts⟩ := EMetric.subset_countable_closure_of_almost_dense_set s h'
exact ⟨t, htc, hts⟩
