English
Let s be a totally bounded subset of a uniform space α. For every entourage U in the uniformity 𝓤 α, there exists a finite subset t ⊆ s such that s is contained in the union, over y in t, of the U-balls around y: s ⊆ ⋃_{y∈t} { x ∈ α : (x,y) ∈ U }.
Русский
Пусть s —TotallyBounded подмножество вершины α униформного пространства. Для каждого окружения U ∈ 𝓤 α существует конечное подмножество t ⊆ s такое, что s ⊆ ⋃_{y∈t} { x ∈ α : (x,y) ∈ U }.
LaTeX
$$$$TotallyBounded(s) \\land (U \\in 𝓤(\\alpha)) \\Rightarrow \\exists t \\subseteq s, \\#t < \\infty \\land s \\subseteq \\bigcup_{y \\in t} \\{ x \\in \\alpha \\mid (x,y) \\in U \\}. $$$$
Lean4
theorem exists_subset {s : Set α} (hs : TotallyBounded s) {U : Set (α × α)} (hU : U ∈ 𝓤 α) :
∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U} :=
by
rcases comp_symm_of_uniformity hU with ⟨r, hr, rs, rU⟩
rcases hs r hr with ⟨k, fk, ks⟩
let u := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
choose f hfs hfr using fun x : u => x.coe_prop.2
refine ⟨range f, ?_, ?_, ?_⟩
· exact range_subset_iff.2 hfs
· haveI : Fintype u := (fk.inter_of_left _).fintype
exact finite_range f
· intro x xs
obtain ⟨y, hy, xy⟩ := mem_iUnion₂.1 (ks xs)
rw [biUnion_range, mem_iUnion]
set z : ↥u := ⟨y, hy, ⟨x, xs, xy⟩⟩
exact ⟨z, rU <| mem_compRel.2 ⟨y, xy, rs (hfr z)⟩⟩
