Topology on the rational numbers

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

instance Rat.instMetricSpaceRat : MetricSpace ℚ

Equations

• Rat.instMetricSpaceRat = MetricSpace.induced Rat.cast Rat.instMetricSpaceRat.proof_1 Real.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 ℚ

Equations

• Rat.instNoncompactSpaceRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRat = (_ : NoncompactSpace ℚ)

theorem Rat.uniformContinuous_add : UniformContinuous fun (p : ℚ × ℚ) => p.1 + p.2

theorem Rat.uniformContinuous_neg : UniformContinuous Neg.neg

instance Rat.instUniformAddGroupRatToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatAddGroup : UniformAddGroup ℚ

Equations

• Rat.instUniformAddGroupRatToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatAddGroup = (_ : UniformAddGroup ℚ)

instance Rat.instTopologicalAddGroupRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatAddGroup : TopologicalAddGroup ℚ

Equations

• Rat.instTopologicalAddGroupRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatAddGroup = (_ : TopologicalAddGroup ℚ)

instance Rat.instOrderTopologyRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatInstPreorderRat : OrderTopology ℚ

Equations

• Rat.instOrderTopologyRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatInstPreorderRat = (_ : OrderTopology ℚ)

theorem Rat.uniformContinuous_abs : UniformContinuous abs

instance Rat.instTopologicalRingRatToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceInstMetricSpaceRatToNonUnitalNonAssocRingToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing : TopologicalRing ℚ

Equations

• One or more equations did not get rendered due to their size.

@[deprecated continuous_mul]

theorem Rat.continuous_mul : Continuous fun (p : ℚ × ℚ) => p.1 * p.2

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