English
Let s be a subset of α. Then s is totally bounded if and only if for every entourage d ∈ 𝓤 α, there exists a finite subset t ⊆ s such that s ⊆ ⋃_{y∈t} { x ∈ α : (x,y) ∈ d }.
Русский
Пусть s ⊆ α. Тогда s полностью ограничено тогда и только тогда, когда для каждого окружения d ∈ 𝓤 α существует конечное подмножество t ⊆ s такое, что s ⊆ ⋃_{y∈t} { x ∈ α : (x,y) ∈ d }.
LaTeX
$$$$TotallyBounded(s) \\iff \\forall d \\in 𝓤(\\alpha), \\exists t \\subseteq s, \\operatorname{Fin}(t) \\land s \\subseteq \\bigcup_{y \\in t} \\{ x \\in \\alpha \\mid (x,y) \\in d \\}. $$$$
Lean4
theorem totallyBounded_iff_subset {s : Set α} :
TotallyBounded s ↔ ∀ d ∈ 𝓤 α, ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d} :=
⟨fun H _ hd ↦ H.exists_subset hd, fun H d hd ↦
let ⟨t, _, ht⟩ := H d hd;
⟨t, ht⟩⟩
