Mathlib.Topology.Instances.Rat

Rat.instMetricSpace instance

: MetricSpace ℚ

Full source

instance : MetricSpace ℚ :=
  MetricSpace.induced (↑) Rat.cast_injective Real.metricSpace

Metric Space Structure on Rational Numbers via Real Embedding

Informal description

The rational numbers $\mathbb{Q}$ form a metric space, where the distance between any two rational numbers $x$ and $y$ is given by the absolute difference of their real number embeddings, $|x - y|$.

Rat.dist_eq theorem

(x y : ℚ) : dist x y = |(x : ℝ) - y|

Full source

theorem dist_eq (x y : ℚ) : dist x y = |(x : ℝ) - y| := rfl

Distance Formula for Rational Numbers via Real Embedding

Informal description

For any two rational numbers $x$ and $y$, the distance between them is equal to the absolute difference of their embeddings in the real numbers, i.e., $\text{dist}(x, y) = |x - y|$.

Rat.dist_cast theorem

(x y : ℚ) : dist (x : ℝ) y = dist x y

Full source

@[norm_cast, simp]
theorem dist_cast (x y : ℚ) : dist (x : ℝ) y = dist x y :=
  rfl

Distance Preservation under Rational-to-Real Embedding

Informal description

For any two rational numbers $x$ and $y$, the distance between their real embeddings $x$ and $y$ in $\mathbb{R}$ is equal to the distance between $x$ and $y$ in $\mathbb{Q}$, i.e., $\text{dist}(x, y) = \text{dist}((x : \mathbb{R}), y)$.

Rat.uniformContinuous_coe_real theorem

: UniformContinuous ((↑) : ℚ → ℝ)

Full source

theorem uniformContinuous_coe_real : UniformContinuous ((↑) : ℚ → ℝ) :=
  uniformContinuous_comap

Uniform Continuity of Rational Embedding into Reals

Informal description

The canonical embedding of the rational numbers $\mathbb{Q}$ into the real numbers $\mathbb{R}$ is uniformly continuous. That is, for any $\epsilon > 0$, there exists $\delta > 0$ such that for all $x, y \in \mathbb{Q}$, if $|x - y| < \delta$, then $|x - y| < \epsilon$ in $\mathbb{R}$.

Rat.isUniformEmbedding_coe_real theorem

: IsUniformEmbedding ((↑) : ℚ → ℝ)

Full source

theorem isUniformEmbedding_coe_real : IsUniformEmbedding ((↑) : ℚ → ℝ) :=
  isUniformEmbedding_comap Rat.cast_injective

Uniform Embedding of Rationals into Reals

Informal description

The canonical embedding of the rational numbers $\mathbb{Q}$ into the real numbers $\mathbb{R}$ is a uniform embedding. That is, it is injective, uniformly continuous, and its inverse is uniformly continuous on its image.

Rat.isDenseEmbedding_coe_real theorem

: IsDenseEmbedding ((↑) : ℚ → ℝ)

Full source

theorem isDenseEmbedding_coe_real : IsDenseEmbedding ((↑) : ℚ → ℝ) :=
  isUniformEmbedding_coe_real.isDenseEmbedding Rat.denseRange_cast

Dense Embedding of Rationals into Reals

Informal description

The canonical embedding of the rational numbers $\mathbb{Q}$ into the real numbers $\mathbb{R}$ is a dense embedding. That is, it is injective, continuous, and its image is dense in $\mathbb{R}$.

Rat.isEmbedding_coe_real theorem

: IsEmbedding ((↑) : ℚ → ℝ)

Full source

theorem isEmbedding_coe_real : IsEmbedding ((↑) : ℚ → ℝ) :=
  isDenseEmbedding_coe_real.isEmbedding

Embedding of Rationals into Reals via Canonical Inclusion

Informal description

The canonical embedding of the rational numbers $\mathbb{Q}$ into the real numbers $\mathbb{R}$ is an embedding. That is, it is injective and continuous, and its inverse is continuous on its image.

Rat.continuous_coe_real theorem

: Continuous ((↑) : ℚ → ℝ)

Full source

theorem continuous_coe_real : Continuous ((↑) : ℚ → ℝ) :=
  uniformContinuous_coe_real.continuous

Continuity of the Rational Embedding into Reals

Informal description

The canonical embedding of the rational numbers $\mathbb{Q}$ into the real numbers $\mathbb{R}$ is continuous. That is, for every $x \in \mathbb{Q}$ and every $\epsilon > 0$, there exists $\delta > 0$ such that for all $y \in \mathbb{Q}$, if $|x - y| < \delta$, then $|x - y| < \epsilon$ in $\mathbb{R}$.

Nat.dist_cast_rat theorem

(x y : ℕ) : dist (x : ℚ) y = dist x y

Full source

@[norm_cast, simp]
theorem Nat.dist_cast_rat (x y : ℕ) : dist (x : ℚ) y = dist x y := by
  rw [← Nat.dist_cast_real, ← Rat.dist_cast]; congr

Distance Preservation When Casting Natural Numbers to Rationals

Informal description

For any natural numbers $x$ and $y$, the distance between $x$ (viewed as a rational number) and $y$ is equal to the distance between $x$ and $y$ as natural numbers, i.e., $\text{dist}(x_\mathbb{Q}, y) = \text{dist}(x, y)$ where $\text{dist}(a,b) = |a - b|$.

Nat.isUniformEmbedding_coe_rat theorem

: IsUniformEmbedding ((↑) : ℕ → ℚ)

Full source

theorem Nat.isUniformEmbedding_coe_rat : IsUniformEmbedding ((↑) : ℕ → ℚ) :=
  isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one <| by simpa using Nat.pairwise_one_le_dist

Uniform Embedding of Natural Numbers into Rationals via Canonical Embedding

Informal description

The canonical embedding of the natural numbers $\mathbb{N}$ into the rational numbers $\mathbb{Q}$ is a uniform embedding. That is, the map $x \mapsto x_\mathbb{Q}$ is injective, uniformly continuous, and its inverse is uniformly continuous on its image.

Nat.isClosedEmbedding_coe_rat theorem

: IsClosedEmbedding ((↑) : ℕ → ℚ)

Full source

theorem Nat.isClosedEmbedding_coe_rat : IsClosedEmbedding ((↑) : ℕ → ℚ) :=
  isClosedEmbedding_of_pairwise_le_dist zero_lt_one <| by simpa using Nat.pairwise_one_le_dist

Natural Number Embedding into Rationals is Closed

Informal description

The canonical embedding of the natural numbers $\mathbb{N}$ into the rational numbers $\mathbb{Q}$ is a closed embedding, meaning it is both a closed map and a topological embedding.

Int.dist_cast_rat theorem

(x y : ℤ) : dist (x : ℚ) y = dist x y

Full source

@[norm_cast, simp]
theorem Int.dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y := by
  rw [← Int.dist_cast_real, ← Rat.dist_cast]; congr

Distance Preservation under Integer-to-Rational Embedding

Informal description

For any two integers $x$ and $y$, the distance between their rational embeddings $x$ and $y$ in $\mathbb{Q}$ is equal to the distance between $x$ and $y$ in $\mathbb{Z}$, i.e., $\text{dist}(x, y) = \text{dist}((x : \mathbb{Q}), y)$.

Int.isUniformEmbedding_coe_rat theorem

: IsUniformEmbedding ((↑) : ℤ → ℚ)

Full source

theorem Int.isUniformEmbedding_coe_rat : IsUniformEmbedding ((↑) : ℤ → ℚ) :=
  isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one <| by simpa using Int.pairwise_one_le_dist

Uniform Embedding of Integers into Rational Numbers

Informal description

The canonical embedding of the integers $\mathbb{Z}$ into the rational numbers $\mathbb{Q}$ is a uniform embedding, meaning it preserves the uniform structure induced by the metric on $\mathbb{Q}$.

Int.isClosedEmbedding_coe_rat theorem

: IsClosedEmbedding ((↑) : ℤ → ℚ)

Full source

theorem Int.isClosedEmbedding_coe_rat : IsClosedEmbedding ((↑) : ℤ → ℚ) :=
  isClosedEmbedding_of_pairwise_le_dist zero_lt_one <| by simpa using Int.pairwise_one_le_dist

Closed Embedding Property of Integer-to-Rational Inclusion

Informal description

The canonical embedding of the integers $\mathbb{Z}$ into the rational numbers $\mathbb{Q}$ is a closed embedding. That is, the map $x \mapsto (x : \mathbb{Q})$ is injective, continuous, and maps closed sets in $\mathbb{Z}$ to closed sets in $\mathbb{Q}$.

Rat.instNoncompactSpace instance

: NoncompactSpace ℚ

Full source

instance : NoncompactSpace ℚ := Int.isClosedEmbedding_coe_rat.noncompactSpace

Noncompactness of the Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ form a noncompact space.

Rat.uniformContinuous_add theorem

: UniformContinuous fun p : ℚ × ℚ => p.1 + p.2

Full source

theorem uniformContinuous_add : UniformContinuous fun p : ℚℚ × ℚ => p.1 + p.2 :=
  Rat.isUniformEmbedding_coe_real.isUniformInducing.uniformContinuous_iff.2 <| by
    simp only [Function.comp_def, Rat.cast_add]
    exact Real.uniformContinuous_add.comp
      (Rat.uniformContinuous_coe_real.prodMap Rat.uniformContinuous_coe_real)

Uniform Continuity of Addition on Rational Numbers

Informal description

The addition operation on the rational numbers $\mathbb{Q}$ is uniformly continuous. That is, the function $(x, y) \mapsto x + y$ from $\mathbb{Q} \times \mathbb{Q}$ to $\mathbb{Q}$ is uniformly continuous with respect to the metric space structure on $\mathbb{Q}$ induced by the canonical embedding into $\mathbb{R}$.

Rat.uniformContinuous_neg theorem

: UniformContinuous (@Neg.neg ℚ _)

Full source

theorem uniformContinuous_neg : UniformContinuous (@Neg.neg ℚ _) :=
  Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨_, ε0, fun _ _ h => by simpa only [abs_sub_comm, dist_eq, cast_neg, neg_sub_neg] using h⟩

Uniform Continuity of Negation on Rational Numbers

Informal description

The negation operation on the rational numbers $\mathbb{Q}$ is uniformly continuous. That is, the function $x \mapsto -x$ from $\mathbb{Q}$ to $\mathbb{Q}$ is uniformly continuous with respect to the metric space structure on $\mathbb{Q}$ induced by the canonical embedding into $\mathbb{R}$.

Rat.instIsUniformAddGroup instance

: IsUniformAddGroup ℚ

Full source

instance : IsUniformAddGroup ℚ :=
  IsUniformAddGroup.mk' Rat.uniformContinuous_add Rat.uniformContinuous_neg

Rational Numbers as a Uniform Additive Group

Informal description

The rational numbers $\mathbb{Q}$ form a uniform additive group with respect to the metric space structure induced from $\mathbb{R}$.

Rat.instIsTopologicalAddGroup instance

: IsTopologicalAddGroup ℚ

Full source

instance : IsTopologicalAddGroup ℚ := inferInstance

Rational Numbers as a Topological Additive Group

Informal description

The rational numbers $\mathbb{Q}$ form a topological additive group with respect to the topology induced by the metric space structure.

Rat.instOrderTopology instance

: OrderTopology ℚ

Full source

instance : OrderTopology ℚ := induced_orderTopology _ Rat.cast_lt exists_rat_btwn

Order Topology on the Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ are equipped with the order topology induced by their natural linear order.

Rat.uniformContinuous_abs theorem

: UniformContinuous (abs : ℚ → ℚ)

Full source

theorem uniformContinuous_abs : UniformContinuous (abs : ℚ → ℚ) :=
  Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨ε, ε0, fun _ _ h =>
      lt_of_le_of_lt (by simpa [Rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _) h⟩

Uniform Continuity of Absolute Value on Rational Numbers

Informal description

The absolute value function $\text{abs} : \mathbb{Q} \to \mathbb{Q}$ is uniformly continuous with respect to the metric space structure on $\mathbb{Q}$ induced by the embedding into $\mathbb{R}$.

Rat.instIsTopologicalRing instance

: IsTopologicalRing ℚ

Full source

instance : IsTopologicalRing ℚ := inferInstance

Topological Ring Structure on Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ form a topological ring with respect to their metric space topology.

Rat.totallyBounded_Icc theorem

(a b : ℚ) : TotallyBounded (Icc a b)

Full source

nonrec theorem totallyBounded_Icc (a b : ℚ) : TotallyBounded (Icc a b) := by
  simpa only [preimage_cast_Icc]
    using totallyBounded_preimage Rat.isUniformEmbedding_coe_real.isUniformInducing
      (totallyBounded_Icc (a : ℝ) b)

Total Boundedness of Closed Rational Intervals

Informal description

For any rational numbers $a$ and $b$, the closed interval $[a, b] \subseteq \mathbb{Q}$ is totally bounded in the metric space of rational numbers.

NNRat.instMetricSpace instance

: MetricSpace ℚ≥0

Full source

instance : MetricSpace ℚ≥0 :=
  Subtype.metricSpace

The Metric Space Structure on Nonnegative Rational Numbers

Informal description

The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ form a metric space, where the distance between any two elements $p$ and $q$ is given by the distance between their embeddings in the metric space of rational numbers.

NNRat.dist_eq theorem

(p q : ℚ≥0) : dist p q = dist (p : ℚ) (q : ℚ)

Full source

@[simp ←, push_cast]
lemma dist_eq (p q : ℚ≥0) : dist p q = dist (p : ℚ) (q : ℚ) := rfl

Distance Preservation in Nonnegative Rationals via Rational Embedding

Informal description

For any two nonnegative rational numbers $p$ and $q$, the distance between $p$ and $q$ in the metric space of nonnegative rational numbers is equal to the distance between their canonical embeddings in the metric space of rational numbers, i.e., $\text{dist}(p, q) = \text{dist}(p, q)$ where the right-hand side is computed in $\mathbb{Q}$.

NNRat.nndist_eq theorem

(p q : ℚ≥0) : nndist p q = nndist (p : ℚ) (q : ℚ)

Full source

@[simp ←, push_cast]
lemma nndist_eq (p q : ℚ≥0) : nndist p q = nndist (p : ℚ) (q : ℚ) := rfl

Nonnegative Distance Preservation in Nonnegative Rationals via Rational Embedding

Informal description

For any two nonnegative rational numbers $p$ and $q$, the nonnegative distance between $p$ and $q$ in the metric space of nonnegative rational numbers is equal to the nonnegative distance between their canonical embeddings in the metric space of rational numbers, i.e., $\text{nndist}(p, q) = \text{nndist}(p, q)$ where the right-hand side is computed in $\mathbb{Q}$.

NNRat.instIsTopologicalSemiring instance

: IsTopologicalSemiring ℚ≥0

Full source

instance : IsTopologicalSemiring ℚ≥0 where
  toContinuousAdd := continuousAdd_induced Nonneg.coeRingHom
  toContinuousMul := continuousMul_induced Nonneg.coeRingHom

Topological Semiring Structure on Nonnegative Rational Numbers

Informal description

The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ form a topological semiring, where both addition and multiplication are continuous operations with respect to the induced topology.

NNRat.instContinuousSub instance

: ContinuousSub ℚ≥0

Full source

instance : ContinuousSub ℚ≥0 :=
  ⟨((continuous_subtype_val.fst'.sub continuous_subtype_val.snd').max
      continuous_const).subtype_mk _⟩

Continuity of Subtraction on Nonnegative Rational Numbers

Informal description

The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ form a topological additive group where the subtraction operation is continuous with respect to the induced topology.

NNRat.instOrderTopology instance

: OrderTopology ℚ≥0

Full source

instance : OrderTopology ℚ≥0 := orderTopology_of_ordConnected (t := Set.Ici 0)

Order Topology on Nonnegative Rational Numbers

Informal description

The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ are equipped with the order topology induced by their natural linear order.

NNRat.instHasContinuousInv₀ instance

: HasContinuousInv₀ ℚ≥0

Full source

instance : HasContinuousInv₀ ℚ≥0 := inferInstance

Continuity of Inversion on Nonzero Nonnegative Rational Numbers

Informal description

The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ have a continuous inversion operation at all nonzero points. That is, the function $x \mapsto x^{-1}$ is continuous on $\mathbb{Q}_{\geq 0} \setminus \{0\}$.