Documentation

Mathlib.Topology.Instances.Rat

Topology on the rational numbers #

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

instance Rat.instMetricSpace :

MetricSpace ℚ

Equations

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.dist ↑x ↑y = Dist.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

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