English
A uniform structure on a set can be built from a distance function that satisfies the metric axioms.
Русский
Единая равномерная структура на множестве строится из функции расстояния, удовлетворяющей аксиомам метрики.
LaTeX
$$$\text{UniformSpace}(\alpha)$ задана через функционал dist:\alpha\times\alpha\to \mathbb{R} и аксиомы симметрии, неотрицательности и треугольного неравенства.$$
Lean4
/-- Construct a uniform structure from a distance function and metric space axioms -/
def ofDist (dist : α → α → ℝ) (dist_self : ∀ x : α, dist x x = 0) (dist_comm : ∀ x y : α, dist x y = dist y x)
(dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : UniformSpace α :=
.ofFun dist dist_self dist_comm dist_triangle ofDist_aux
