Topology on the rational numbers #
The structure of a metric space on ℚ
is introduced in this file, induced from ℝ
.
Equations
@[deprecated Rat.isUniformEmbedding_coe_real]
Alias of Rat.isUniformEmbedding_coe_real
.
@[deprecated Rat.isDenseEmbedding_coe_real]
Alias of Rat.isDenseEmbedding_coe_real
.
@[deprecated Nat.isUniformEmbedding_coe_rat]
Alias of Nat.isUniformEmbedding_coe_rat
.
@[deprecated Int.isUniformEmbedding_coe_rat]
Alias of Int.isUniformEmbedding_coe_rat
.