Topology on the rational numbers

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

instance Rat.instMetricSpace : MetricSpace ℚ

Equations

• Rat.instMetricSpace = MetricSpace.induced Rat.cast Rat.instMetricSpace.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.isUniformEmbedding_coe_real : IsUniformEmbedding Rat.cast

@[deprecated Rat.isUniformEmbedding_coe_real]

theorem Rat.uniformEmbedding_coe_real : IsUniformEmbedding Rat.cast

Alias of Rat.isUniformEmbedding_coe_real.

theorem Rat.isDenseEmbedding_coe_real : IsDenseEmbedding Rat.cast

@[deprecated Rat.isDenseEmbedding_coe_real]

theorem Rat.denseEmbedding_coe_real : IsDenseEmbedding Rat.cast

Alias of Rat.isDenseEmbedding_coe_real.

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.isUniformEmbedding_coe_rat : IsUniformEmbedding Nat.cast

@[deprecated Nat.isUniformEmbedding_coe_rat]

theorem Nat.uniformEmbedding_coe_rat : IsUniformEmbedding Nat.cast

Alias of Nat.isUniformEmbedding_coe_rat.

theorem Nat.closedEmbedding_coe_rat : ClosedEmbedding Nat.cast

@[simp]

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

theorem Int.isUniformEmbedding_coe_rat : IsUniformEmbedding Int.cast

@[deprecated Int.isUniformEmbedding_coe_rat]

theorem Int.uniformEmbedding_coe_rat : IsUniformEmbedding Int.cast

Alias of Int.isUniformEmbedding_coe_rat.

theorem Int.closedEmbedding_coe_rat : ClosedEmbedding Int.cast

instance Rat.instNoncompactSpace : NoncompactSpace ℚ

Equations

• Rat.instNoncompactSpace = ⋯

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

theorem Rat.uniformContinuous_neg : UniformContinuous Neg.neg

instance Rat.instUniformAddGroup : UniformAddGroup ℚ

Equations

• Rat.instUniformAddGroup = ⋯

instance Rat.instTopologicalAddGroup : TopologicalAddGroup ℚ

Equations

• Rat.instTopologicalAddGroup = ⋯

instance Rat.instOrderTopology : OrderTopology ℚ

Equations

• Rat.instOrderTopology = ⋯

theorem Rat.uniformContinuous_abs : UniformContinuous abs

instance Rat.instTopologicalRing : TopologicalRing ℚ

Equations

• Rat.instTopologicalRing = ⋯

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