Topology on the rational numbers

The structure of a metric space on ℚ is introduced in this file, induced from ℝ.

instance Rat.instMetricSpaceRat : MetricSpace ℚ

theorem Rat.dist_eq (x : ℚ) (y : ℚ) : dist x y = |↑x - ↑y|

@[simp]

theorem Rat.dist_cast (x : ℚ) (y : ℚ) : dist ↑x ↑y = dist x y

theorem Rat.uniformContinuous_coe_real : UniformContinuous Rat.cast

theorem Rat.uniformEmbedding_coe_real : UniformEmbedding Rat.cast

theorem Rat.denseEmbedding_coe_real : DenseEmbedding Rat.cast

theorem Rat.embedding_coe_real : Embedding Rat.cast

theorem Rat.continuous_coe_real : Continuous Rat.cast

@[simp]

theorem Nat.dist_cast_rat (x : ℕ) (y : ℕ) : dist ↑x ↑y = dist x y

theorem Nat.uniformEmbedding_coe_rat : UniformEmbedding Nat.cast

theorem Nat.closedEmbedding_coe_rat : ClosedEmbedding Nat.cast

@[simp]

theorem Int.dist_cast_rat (x : ℤ) (y : ℤ) : dist ↑x ↑y = dist x y

theorem Int.uniformEmbedding_coe_rat : UniformEmbedding Int.cast

theorem Int.closedEmbedding_coe_rat : ClosedEmbedding Int.cast

instance Rat.instNoncompactSpaceRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRat : NoncompactSpace ℚ

theorem Rat.uniformContinuous_add : UniformContinuous fun p => p.fst + p.snd

theorem Rat.uniformContinuous_neg : UniformContinuous Neg.neg

instance Rat.instUniformAddGroupRatToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatAddGroup : UniformAddGroup ℚ

instance Rat.instTopologicalAddGroupRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatAddGroup : TopologicalAddGroup ℚ

instance Rat.instOrderTopologyRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatInstPreorderRat : OrderTopology ℚ

theorem Rat.uniformContinuous_abs : UniformContinuous abs

instance Rat.instTopologicalRingRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatToNonUnitalNonAssocRingToNonAssocRingToRingDivisionRing : TopologicalRing ℚ

@[deprecated continuous_mul]

theorem Rat.continuous_mul : Continuous fun p => p.fst * p.snd

theorem Rat.totallyBounded_Icc (a : ℚ) (b : ℚ) : TotallyBounded (Set.Icc a b)