Topology on the rational numbers #
The structure of a metric space on ℚ
is introduced in this file, induced from ℝ
.
@[deprecated Rat.isEmbedding_coe_real (since := "2024-10-26")]
Alias of Rat.isEmbedding_coe_real
.
The structure of a metric space on ℚ
is introduced in this file, induced from ℝ
.
Alias of Rat.isEmbedding_coe_real
.