English
There is a general construction UniformSpace.ofFun that builds a UniformSpace on X from a distance-like function d: X×X → M together with axioms: reflexivity, symmetry, triangle inequality, and a half-continuity condition.
Русский
Существует общая конструкция UniformSpace.ofFun, которая задаёт униформное пространство на X через функцию d: X×X → M с аксиомами: рефлексивность, симметрия, неравенство треугольника и половинная непрерывность.
LaTeX
$$$\text{UniformSpace}(X) = \text{ofFun}(d, \text{refl}, \text{symm}, \text{triangle}, \text{half})$$$
Lean4
/-- Define a `UniformSpace` using a "distance" function. The function can be, e.g., the
distance in a (usual or extended) metric space or an absolute value on a ring. We assume that
there is a preexisting topology, for which the neighborhoods can be expressed using the "distance",
and we make sure that the uniform space structure we construct has a topology which is defeq
to the original one. -/
def ofFunOfHasBasis [t : TopologicalSpace X] [AddCommMonoid M] [LinearOrder M] (d : X → X → M) (refl : ∀ x, d x x = 0)
(symm : ∀ x y, d x y = d y x) (triangle : ∀ x y z, d x z ≤ d x y + d y z)
(half : ∀ ε > (0 : M), ∃ δ > (0 : M), ∀ x < δ, ∀ y < δ, x + y < ε)
(basis : ∀ x, (𝓝 x).HasBasis (fun ε ↦ 0 < ε) (fun ε ↦ {y | d x y < ε})) : UniformSpace X
where
toTopologicalSpace := t
nhds_eq_comap_uniformity
x := (basis x).eq_of_same_basis <| (hasBasis_ofFun (basis x).ex_mem d refl symm triangle half).comap (Prod.mk x)
__ := ofFun d refl symm triangle half
