Mathlib.Topology.Instances.Rat
source
The structure of a metric space on ℚ is introduced in this file, induced from ℝ.
ℚ
ℝ