# mathlibdocumentation

topology.uniform_space.absolute_value

# 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.

## Implementation details #

Note that we import data.real.cau_seq because this is where absolute values are defined, but the current file does not depend on real numbers. TODO: extract absolute values from that data.real folder.

## Tags #

absolute value, uniform spaces

def is_absolute_value.uniform_space_core {π : Type u_1} [linear_ordered_field π] {R : Type u_2} [comm_ring R] (abv : R β π) [is_absolute_value abv] :

The uniformity coming from an absolute value.

Equations
def is_absolute_value.uniform_space {π : Type u_1} [linear_ordered_field π] {R : Type u_2} [comm_ring R] (abv : R β π) [is_absolute_value abv] :

The uniform structure coming from an absolute value.

Equations
theorem is_absolute_value.mem_uniformity {π : Type u_1} [linear_ordered_field π] {R : Type u_2} [comm_ring R] (abv : R β π) [is_absolute_value abv] {s : set (R Γ R)} :
β β (Ξ΅ : π) (H : Ξ΅ > 0), β {a b : R}, abv (b - a) < Ξ΅ β (a, b) β s