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

theorem Rat.isDenseEmbedding_coe_real : IsDenseEmbedding Rat.cast

theorem Rat.isEmbedding_coe_real : Topology.IsEmbedding 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

theorem Nat.isClosedEmbedding_coe_rat : Topology.IsClosedEmbedding Nat.cast

@[simp]

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

theorem Int.isUniformEmbedding_coe_rat : IsUniformEmbedding Int.cast

theorem Int.isClosedEmbedding_coe_rat : Topology.IsClosedEmbedding Int.cast

instance Rat.instNoncompactSpace : NoncompactSpace ℚ

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

theorem Rat.uniformContinuous_neg : UniformContinuous Neg.neg

instance Rat.instIsUniformAddGroup : IsUniformAddGroup ℚ

instance Rat.instIsTopologicalAddGroup : IsTopologicalAddGroup ℚ

instance Rat.instOrderTopology : OrderTopology ℚ

theorem Rat.uniformContinuous_abs : UniformContinuous abs

instance Rat.instIsTopologicalRing : IsTopologicalRing ℚ

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

instance NNRat.instMetricSpace : MetricSpace ℚ≥0

Equations

• NNRat.instMetricSpace = Subtype.metricSpace

theorem NNRat.dist_eq (p q : ℚ≥0) : dist p q = dist ↑p ↑q

theorem NNRat.nndist_eq (p q : ℚ≥0) : nndist p q = nndist ↑p ↑q

instance NNRat.instIsTopologicalSemiring : IsTopologicalSemiring ℚ≥0

instance NNRat.instContinuousSub : ContinuousSub ℚ≥0

instance NNRat.instOrderTopology : OrderTopology ℚ≥0

instance NNRat.instContinuousInv₀ : ContinuousInv₀ ℚ≥0

instance NNRat.instContinuousSMulRatReal : ContinuousSMul ℚ ℝ

instance NNRat.instContinuousSMulOfIsScalarTowerOfRat {R : Type u_1} [TopologicalSpace R] [MulAction ℚ R] [MulAction ℚ≥0 R] [IsScalarTower ℚ≥0 ℚ R] [ContinuousSMul ℚ R] : ContinuousSMul ℚ≥0 R

instance NNRat.instContinuousSMulNNReal : ContinuousSMul ℚ≥0 NNReal