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

def UniformSpace.ofFun {X : Type u_1} {M : Type u_2} [OrderedAddCommMonoid 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} [LinearOrderedAddCommMonoid 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 < ε}