English
Membership in the uniformity U is characterized by existence of ε>0 with a distance bound for all pairs.
Русский
Членство в равномерности характеризуется существованием ε>0 с ограничением расстояния для всех пар.
LaTeX
$$$ s ∈ 𝓤 α \iff \exists ε > 0, \forall {a,b}, edist a b < ε \Rightarrow (a,b) ∈ s $$$
Lean4
/-- Characterization of the elements of the uniformity in terms of the extended distance -/
theorem mem_uniformity_edist {s : Set (α × α)} : s ∈ 𝓤 α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s :=
uniformity_basis_edist.mem_uniformity_iff