English
A subset s of a pseudo-emetric space is totally bounded iff for every ε > 0 there exists a finite set of centers t such that s is contained in the union over y ∈ t of balls B(y, ε).
Русский
Множество s в псевдоэметрическом пространстве полностью ограничено тогда и только тогда, когда для каждого ε > 0 существует конечное множество центров t such that s ⊆ ⋃_{y∈t} B(y, ε).
LaTeX
$$TotallyBounded s ↔ ∀ ε > 0, ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε$$
Lean4
theorem totallyBounded_iff {s : Set α} : TotallyBounded s ↔ ∀ ε > 0, ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε :=
⟨fun H _ε ε0 => H _ (edist_mem_uniformity ε0), fun H _r ru =>
let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru
let ⟨t, ft, h⟩ := H ε ε0
⟨t, ft, h.trans <| iUnion₂_mono fun _ _ _ => hε⟩⟩
