Construct a UniformSpace from a dist-like function

In this file we provide a constructor for UniformSpace given a dist-like function

TODO

RFC: use UniformSpace.Core.mkOfBasis? This will change defeq here and there

@[instance_reducible]

def UniformSpace.ofFun {X : Type u_1} {M : Type u_2} [AddCommMonoid M] [PartialOrder M] (d : X → X → M) (refl : ∀ (x : X), d x x = 0) (symm : ∀ (x y : X), d x y = d y x) (triangle : ∀ (x y z : X), d x z ≤ d x y + d y z) (half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε) : UniformSpace X

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.

Equations

• One or more equations did not get rendered due to their size.

theorem UniformSpace.hasBasis_ofFun {X : Type u_1} {M : Type u_2} [AddCommMonoid M] [LinearOrder M] (h₀ : ∃ (x : M), 0 < x) (d : X → X → M) (refl : ∀ (x : X), d x x = 0) (symm : ∀ (x y : X), d x y = d y x) (triangle : ∀ (x y z : X), d x z ≤ d x y + d y z) (half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε) : (uniformity X).HasBasis (fun (x : M) => 0 < x) fun (ε : M) => {x : X × X | d x.1 x.2 < ε}

@[instance_reducible]

def UniformSpace.ofFunOfHasBasis {X : Type u_1} {M : Type u_2} [t : TopologicalSpace X] [AddCommMonoid M] [LinearOrder M] (d : X → X → M) (refl : ∀ (x : X), d x x = 0) (symm : ∀ (x y : X), d x y = d y x) (triangle : ∀ (x y z : X), d x z ≤ d x y + d y z) (half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε) (basis : ∀ (x : X), (nhds x).HasBasis (fun (ε : M) => 0 < ε) fun (ε : M) => {y : X | d x y < ε}) : UniformSpace X

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.

Equations

• UniformSpace.ofFunOfHasBasis d refl symm triangle half basis = { toTopologicalSpace := t, uniformity := UniformSpace.uniformity, symm := ⋯, comp := ⋯, nhds_eq_comap_uniformity := ⋯ }