Documentation

Mathlib.Topology.Instances.Rat

Topology on the rational numbers #

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

source
instance Rat.instMetricSpace :
MetricSpace ℚ
Equations
source
theorem Rat.dist_eq (x y : ℚ) :
dist x y = |↑x - ↑y|
source
@[simp]
theorem Rat.dist_cast (x y : ℚ) :
dist ↑x ↑y = dist x y
source
theorem Rat.uniformContinuous_coe_real :
UniformContinuous Rat.cast
source
theorem Rat.isUniformEmbedding_coe_real :
IsUniformEmbedding Rat.cast
source
@[deprecated Rat.isUniformEmbedding_coe_real (since := "2024-10-01")]
theorem Rat.uniformEmbedding_coe_real :
IsUniformEmbedding Rat.cast

Alias of Rat.isUniformEmbedding_coe_real.

source
theorem Rat.isDenseEmbedding_coe_real :
IsDenseEmbedding Rat.cast
source
theorem Rat.isEmbedding_coe_real :
Topology.IsEmbedding Rat.cast
source
@[deprecated Rat.isEmbedding_coe_real (since := "2024-10-26")]
theorem Rat.embedding_coe_real :
Topology.IsEmbedding Rat.cast

Alias of Rat.isEmbedding_coe_real.

source
theorem Rat.continuous_coe_real :
Continuous Rat.cast
source
@[simp]
theorem Nat.dist_cast_rat (x y : ℕ) :
dist ↑x ↑y = dist x y
source
theorem Nat.isUniformEmbedding_coe_rat :
IsUniformEmbedding Nat.cast
source
@[deprecated Nat.isUniformEmbedding_coe_rat (since := "2024-10-01")]
theorem Nat.uniformEmbedding_coe_rat :
IsUniformEmbedding Nat.cast

Alias of Nat.isUniformEmbedding_coe_rat.

source
theorem Nat.isClosedEmbedding_coe_rat :
Topology.IsClosedEmbedding Nat.cast
source
@[deprecated Nat.isClosedEmbedding_coe_rat (since := "2024-10-20")]
theorem Nat.closedEmbedding_coe_rat :
Topology.IsClosedEmbedding Nat.cast

Alias of Nat.isClosedEmbedding_coe_rat.

source
@[simp]
theorem Int.dist_cast_rat (x y : ℤ) :
dist ↑x ↑y = dist x y
source
theorem Int.isUniformEmbedding_coe_rat :
IsUniformEmbedding Int.cast
source
@[deprecated Int.isUniformEmbedding_coe_rat (since := "2024-10-01")]
theorem Int.uniformEmbedding_coe_rat :
IsUniformEmbedding Int.cast

Alias of Int.isUniformEmbedding_coe_rat.

source
theorem Int.isClosedEmbedding_coe_rat :
Topology.IsClosedEmbedding Int.cast
source
@[deprecated Int.isClosedEmbedding_coe_rat (since := "2024-10-20")]
theorem Int.closedEmbedding_coe_rat :
Topology.IsClosedEmbedding Int.cast

Alias of Int.isClosedEmbedding_coe_rat.

source
instance Rat.instNoncompactSpace :
NoncompactSpace ℚ
source
theorem Rat.uniformContinuous_add :
UniformContinuous fun (p : ℚ × ℚ) => p.1 + p.2
source
theorem Rat.uniformContinuous_neg :
UniformContinuous Neg.neg
source
instance Rat.instIsUniformAddGroup :
IsUniformAddGroup ℚ
source
instance Rat.instIsTopologicalAddGroup :
IsTopologicalAddGroup ℚ
source
instance Rat.instOrderTopology :
OrderTopology ℚ
source
theorem Rat.uniformContinuous_abs :
UniformContinuous abs
source
instance Rat.instIsTopologicalRing :
IsTopologicalRing ℚ
source
theorem Rat.totallyBounded_Icc (a b : ℚ) :
TotallyBounded (Set.Icc a b)
source
instance NNRat.instMetricSpace :
MetricSpace ℚ≥0
Equations
source
theorem NNRat.dist_eq (p q : ℚ≥0) :
dist p q = dist ↑p ↑q
source
theorem NNRat.nndist_eq (p q : ℚ≥0) :
nndist p q = nndist ↑p ↑q
source
instance NNRat.instIsTopologicalSemiring :
IsTopologicalSemiring ℚ≥0
source
instance NNRat.instContinuousSub :
ContinuousSub ℚ≥0
source
instance NNRat.instOrderTopology :
OrderTopology ℚ≥0
source
instance NNRat.instHasContinuousInv₀ :
HasContinuousInv₀ ℚ≥0