mathlib3 documentation


Uniform structure induced by an absolute value #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 absolute_value.uniform_space {𝕜 : Type u_1} [linear_ordered_field 𝕜] {R : Type u_2} [comm_ring R] (abv : absolute_value R 𝕜) :

The uniform space structure coming from an absolute value.

theorem absolute_value.has_basis_uniformity {𝕜 : Type u_1} [linear_ordered_field 𝕜] {R : Type u_2} [comm_ring R] (abv : absolute_value R 𝕜) :
(uniformity R).has_basis (λ (ε : 𝕜), 0 < ε) (λ (ε : 𝕜), {p : R × R | abv (p.snd - p.fst) < ε})