English
A set s is totally bounded if for every entourage d there exists a finite set t such that every element of s is d-close to some element of t.
Русский
Множество s totally bounded, если для каждого окружения d существует конечное множество t, такое что каждый элемент s d-близок к некоторому элементу t.
LaTeX
$$$TotallyBounded(s) \\iff \\forall d \\in 𝓤(\\alpha), \\exists t: Set(\\alpha), t. Finite \\land s \\subseteq \\bigcup_{y\\in t} \\{x\\mid (x,y)\\in d\\}$$$
Lean4
/-- A set `s` is totally bounded if for every entourage `d` there is a finite
set of points `t` such that every element of `s` is `d`-near to some element of `t`. -/
def TotallyBounded (s : Set α) : Prop :=
∀ d ∈ 𝓤 α, ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
