English
The uniform space structure on ℚ induced by the absolute value coincides with the standard uniform structure coming from the real numbers when embedding ℚ into ℝ.
Русский
Униформная структура на ℚ, заданная через модуль, совпадает с обычной униформностью через внедрение ℚ в ℝ.
LaTeX
$$$(|\cdot| : \mathbb{Q} \to \mathbb{Q}).\text{uniformSpace} = \text{PseudoMetricSpace}.toUniformSpace$$$
Lean4
/-- The metric space uniform structure on ℚ (which presupposes the existence
of real numbers) agrees with the one coming directly from (abs : ℚ → ℚ). -/
theorem uniformSpace_eq : (AbsoluteValue.abs : AbsoluteValue ℚ ℚ).uniformSpace = PseudoMetricSpace.toUniformSpace :=
by
ext s
rw [(AbsoluteValue.hasBasis_uniformity _).mem_iff, Metric.uniformity_basis_dist_rat.mem_iff]
simp only [Rat.dist_eq, AbsoluteValue.abs_apply, ← Rat.cast_sub, ← Rat.cast_abs, Rat.cast_lt, abs_sub_comm]
