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

## References

• [N. Bourbaki, Topologie générale][bourbaki1966]

## Tags

absolute value, uniform spaces

def is_absolute_value.uniform_space_core {𝕜 : Type u_1} {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} {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} {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