English
Let HasBasis H of the uniformity be given by a family (p, U). Then totally boundedness of s is equivalent to: for every i with p(i), there exists a finite t ⊆ s such that s ⊆ ⋃_{y∈t} { x ∈ α : (x,y) ∈ U_i }.
Русский
Пусть база H униформности задана парой (p, U). Тогда полная ограниченность s эквивалентна тому, что для каждого i с p(i) существует конечное t ⊆ s такое, что s ⊆ ⋃_{y∈t} { x ∈ α : (x,y) ∈ U_i }.
LaTeX
$$$$TotallyBounded(s) \\iff \\forall i, p(i) \\to \\exists t \\subseteq s, \\operatorname{Fin}(t) \\land s \\subseteq \\bigcup_{y \\in t} \\{ x \\in \\alpha \\mid (x,y) \\in U_i \\}. $$$$
Lean4
theorem totallyBounded_iff {ι} {p : ι → Prop} {U : ι → Set (α × α)} (H : (𝓤 α).HasBasis p U) {s : Set α} :
TotallyBounded s ↔ ∀ i, p i → ∃ t : Set α, Set.Finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i} :=
H.forall_iff fun _ _ hUV h => h.imp fun _ ht => ⟨ht.1, ht.2.trans <| iUnion₂_mono fun _ _ _ hy => hUV hy⟩
