English
If a set s satisfies that for every symmetric entourage V ∈ 𝓤 α there exists a finite t with s ⊆ ⋃_{y∈t} Ball(y,V), then s is totally bounded.
Русский
Если для каждого симметричного окружения V ∈ 𝓤 α существует конечное t такое, что s ⊆ ⋃_{y∈t} Ball(y,V), то s полностью ограничено.
LaTeX
$$$$\\forall V \\in 𝓤(\\alpha), \\mathrm{IsSymmetricRel}(V) \\Rightarrow \\exists t \\subseteq s, \\operatorname{Fin}(t) \\land s \\subseteq \\bigcup_{y \\in t} \\mathrm{Ball}(y,V). $$$$
Lean4
theorem totallyBounded_of_forall_symm {s : Set α}
(h : ∀ V ∈ 𝓤 α, IsSymmetricRel V → ∃ t : Set α, Set.Finite t ∧ s ⊆ ⋃ y ∈ t, ball y V) : TotallyBounded s :=
UniformSpace.hasBasis_symmetric.totallyBounded_iff.2 fun V hV => by
simpa only [ball_eq_of_symmetry hV.2] using h V hV.1 hV.2
