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
@[protected]
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.
Equations
- abv.uniform_space = uniform_space.of_fun (λ (x y : R), ⇑abv (y - x)) _ _ _ absolute_value.uniform_space._proof_4
theorem
absolute_value.has_basis_uniformity
{𝕜 : Type u_1}
[linear_ordered_field 𝕜]
{R : Type u_2}
[comm_ring R]
(abv : absolute_value R 𝕜) :