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

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

@[deprecated Rat.isEmbedding_coe_real (since := "2024-10-26")]

theorem Rat.embedding_coe_real :

Topology.IsEmbedding Rat.cast

Alias of Rat.isEmbedding_coe_real.

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.instHasContinuousInv₀ :

HasContinuousInv₀ ℚ≥0