Rat.uniformSpace_eq

theorem Rat.uniformSpace_eq : AbsoluteValue.abs.uniformSpace = PseudoMetricSpace.toUniformSpace

This theorem states that the uniform structure on the set of rational numbers, which is inferred from the metric space structure (which in turn presupposes the existence of real numbers), is equivalent to the one obtained directly from the absolute value function mapping rational numbers to rational numbers. In other words, when we consider the set of rational numbers as a metric space, the uniform structure derived from that view is the same as if we had simply used the absolute value function on the rational numbers.

More concisely: The uniform structures on the rational numbers as a metric space and as the set equipped with the absolute value function are equivalent.