doc-next-gen

Mathlib.Topology.Instances.Nat

Module docstring

{"# Topology on the natural numbers

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

Nat.instDist instance
: Dist ℕ
Full source 
noncomputable instance : Dist ℕ :=
  ⟨fun x y => dist (x : ℝ) y⟩
The Distance Function on Natural Numbers
Informal description
The natural numbers $\mathbb{N}$ are equipped with a distance function $dist : \mathbb{N} \to \mathbb{N} \to \mathbb{R}$ defined by $dist(x, y) = |x - y|$, where $x$ and $y$ are viewed as real numbers.
Nat.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 Natural Numbers via Real Casting
Informal description
For any natural numbers $x$ and $y$, the distance between $x$ and $y$ is equal to the absolute value of their difference when viewed as real numbers, i.e., $\text{dist}(x, y) = |x - y|$.
Nat.dist_coe_int theorem
(x y : ℕ) : dist (x : ℤ) (y : ℤ) = dist x y
Full source 
theorem dist_coe_int (x y : ℕ) : dist (x : ℤ) (y : ℤ) = dist x y := rfl
Distance Preservation under Integer Casting of Natural Numbers
Informal description
For any natural numbers $x$ and $y$, the distance between their integer casts equals the distance between $x$ and $y$ as natural numbers, i.e., $\text{dist}((x : \mathbb{Z}), (y : \mathbb{Z})) = \text{dist}(x, y)$.
Nat.dist_cast_real theorem
(x y : ℕ) : dist (x : ℝ) y = dist x y
Full source 
@[norm_cast, simp]
theorem dist_cast_real (x y : ℕ) : dist (x : ℝ) y = dist x y := rfl
Distance Preservation When Casting Natural Numbers to Reals
Informal description
For any natural numbers $x$ and $y$, the distance between $x$ (viewed as a real number) and $y$ is equal to the distance between $x$ and $y$ as natural numbers, i.e., $\text{dist}(x_\mathbb{R}, y) = \text{dist}(x, y)$ where $\text{dist}(a,b) = |a - b|$.
Nat.pairwise_one_le_dist theorem
: Pairwise fun m n : ℕ => 1 ≤ dist m n
Full source 
theorem pairwise_one_le_dist : Pairwise fun m n : ℕ => 1 ≤ dist m n := fun _ _ hne =>
  Int.pairwise_one_le_dist <| mod_cast hne
Minimum Distance Between Distinct Natural Numbers is 1
Informal description
For any two distinct natural numbers $m$ and $n$, the distance between them is at least 1, i.e., $|m - n| \geq 1$.
Nat.isUniformEmbedding_coe_real theorem
: IsUniformEmbedding ((↑) : ℕ → ℝ)
Full source 
theorem isUniformEmbedding_coe_real : IsUniformEmbedding ((↑) : ℕ → ℝ) :=
  isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
Uniform Embedding of Natural Numbers into Reals via Inclusion
Informal description
The canonical embedding of the natural numbers into the real numbers, given by the inclusion map $(\cdot) : \mathbb{N} \to \mathbb{R}$, is a uniform embedding. That is, it is injective, uniformly continuous, and its inverse is uniformly continuous on its image.
Nat.isClosedEmbedding_coe_real theorem
: IsClosedEmbedding ((↑) : ℕ → ℝ)
Full source 
theorem isClosedEmbedding_coe_real : IsClosedEmbedding ((↑) : ℕ → ℝ) :=
  isClosedEmbedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
Closed Embedding of Natural Numbers into Reals via Inclusion
Informal description
The canonical embedding of the natural numbers into the real numbers, given by the inclusion map $n \mapsto n$, is a closed embedding. This means it is both a topological embedding (homeomorphism onto its image) and has closed image in $\mathbb{R}$.
Nat.instMetricSpace instance
: MetricSpace ℕ
Full source 
instance : MetricSpace ℕ := Nat.isUniformEmbedding_coe_real.comapMetricSpace _
The Metric Space Structure on Natural Numbers
Informal description
The natural numbers $\mathbb{N}$ are equipped with a canonical metric space structure, which is induced from the metric space structure of the real numbers via the inclusion map.
Nat.preimage_ball theorem
(x : ℕ) (r : ℝ) : (↑) ⁻¹' ball (x : ℝ) r = ball x r
Full source 
theorem preimage_ball (x : ℕ) (r : ℝ) : (↑) ⁻¹' ball (x : ℝ) r = ball x r := rfl
Preimage of Open Ball in Natural Numbers Matches Induced Open Ball
Informal description
For any natural number $x$ and real number $r$, the preimage of the open ball $\text{ball}(x, r)$ in $\mathbb{R}$ under the canonical inclusion map $\mathbb{N} \hookrightarrow \mathbb{R}$ is equal to the open ball $\text{ball}(x, r)$ in $\mathbb{N}$ with the induced metric. That is, $\{n \in \mathbb{N} \mid n \in \text{ball}(x, r)\} = \text{ball}(x, r) \cap \mathbb{N}$.
Nat.preimage_closedBall theorem
(x : ℕ) (r : ℝ) : (↑) ⁻¹' closedBall (x : ℝ) r = closedBall x r
Full source 
theorem preimage_closedBall (x : ℕ) (r : ℝ) : (↑) ⁻¹' closedBall (x : ℝ) r = closedBall x r := rfl
Preimage of Closed Ball in Natural Numbers Matches Induced Closed Ball
Informal description
For any natural number $x$ and real number $r$, the preimage of the closed ball $\overline{B}(x, r)$ in $\mathbb{R}$ under the canonical inclusion map $\mathbb{N} \hookrightarrow \mathbb{R}$ is equal to the closed ball $\overline{B}(x, r)$ in $\mathbb{N}$ with the induced metric. That is, $\{n \in \mathbb{N} \mid n \in \overline{B}(x, r)\} = \overline{B}(x, r) \cap \mathbb{N}$.
Nat.closedBall_eq_Icc theorem
(x : ℕ) (r : ℝ) : closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
Full source 
theorem closedBall_eq_Icc (x : ℕ) (r : ℝ) : closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊ := by
  rcases le_or_lt 0 r with (hr | hr)
  · rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
    exact add_nonneg (cast_nonneg x) hr
  · rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]
    calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
    _ < ⌈↑x - r⌉₊ := by
      rw [floor_natCast, Nat.lt_ceil]
      linarith
Closed Ball in Natural Numbers Equals Ceiling-Floor Interval
Informal description
For any natural number $x$ and real number $r$, the closed ball $\overline{B}(x, r)$ in the natural numbers with the metric induced from $\mathbb{R}$ is equal to the closed interval $[\lceil x - r \rceil, \lfloor x + r \rfloor]$, where $\lceil \cdot \rceil$ and $\lfloor \cdot \rfloor$ denote the ceiling and floor functions respectively.