Documentation

Mathlib.Topology.UniformSpace.AbsoluteValue

Uniform structure induced by an absolute value #

We build a uniform space structure on a commutative ring R equipped with an absolute value into a linear ordered field π•œ. Of course in the case R is β„š, ℝ or β„‚ and π•œ = ℝ, we get the same thing as the metric space construction, and the general construction follows exactly the same path.

References #

Tags #

absolute value, uniform spaces

def AbsoluteValue.uniformSpace {π•œ : Type u_1} [LinearOrderedField π•œ] {R : Type u_2} [CommRing R] (abv : AbsoluteValue R π•œ) :

The uniform structure coming from an absolute value.

Equations
  • abv.uniformSpace = UniformSpace.ofFun (fun (x y : R) => abv (y - x)) β‹― β‹― β‹― β‹―
Instances For
    theorem AbsoluteValue.hasBasis_uniformity {π•œ : Type u_1} [LinearOrderedField π•œ] {R : Type u_2} [CommRing R] (abv : AbsoluteValue R π•œ) :
    (uniformity R).HasBasis (fun (x : π•œ) => 0 < x) fun (Ξ΅ : π•œ) => {p : R Γ— R | abv (p.2 - p.1) < Ξ΅}