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
𝕜 = ℝ, we get the same thing as the metric space construction, and the general construction
follows exactly the same path.
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
- [N. Bourbaki, Topologie générale][bourbaki1966]
absolute value, uniform spaces
The uniformity coming from an absolute value.
The uniform structure coming from an absolute value.