mathlib documentation

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

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)} :
s ∈ (is_absolute_value.uniform_space_core abv).uniformity ↔ βˆƒ (Ξ΅ : π•œ) (H : Ξ΅ > 0), βˆ€ {a b : R}, abv (b - a) < Ξ΅ β†’ (a, b) ∈ s