Theorems · Theorem · general topology

UniformSpace.hasBasis_ofFun

∀ {X : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder M],
  (∃ x, 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 => 0 < x) fun ε => {x | d x.1 x.2 < ε}

Defined in

Mathlib.Topology.UniformSpace.OfFun

Cited by

3 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidLinearOrder