Mathlib.Topology.Instances.Int

Int.instDist instance

: Dist ℤ

Full source

instance : Dist ℤ :=
  ⟨fun x y => dist (x : ℝ) y⟩

The Distance Function on Integers Induced from Real Numbers

Informal description

The integers $\mathbb{Z}$ are equipped with a distance function $dist : \mathbb{Z} \to \mathbb{Z} \to \mathbb{R}$ defined by $dist(x, y) = |x - y|$, where $x$ and $y$ are viewed as real numbers.

Int.dist_eq theorem

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

Full source

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

Distance on Integers via Real Embedding: $\text{dist}(x, y) = |x_\mathbb{R} - y|$

Informal description

For any integers $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_\mathbb{R} - y|$ where $x_\mathbb{R}$ denotes the embedding of $x$ in $\mathbb{R}$.

Int.dist_eq' theorem

(m n : ℤ) : dist m n = |m - n|

Full source

theorem dist_eq' (m n : ℤ) : dist m n = |m - n| := by rw [dist_eq]; norm_cast

Distance Formula for Integers: $\text{dist}(m, n) = |m - n|$

Informal description

For any integers $m$ and $n$, the distance between $m$ and $n$ is equal to the absolute value of their difference, i.e., $\text{dist}(m, n) = |m - n|$.

Int.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 under Integer-to-Real Embedding

Informal description

For any integers $x$ and $y$, the distance between their real number embeddings equals the distance between the integers themselves, i.e., $\text{dist}(x_\mathbb{R}, y) = \text{dist}(x, y)$ where $x_\mathbb{R}$ denotes the real number obtained by embedding $x$ into $\mathbb{R}$.

Int.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 := by
  intro m n hne
  rw [dist_eq]; norm_cast; rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]

Minimum Distance Between Distinct Integers: $\text{dist}(m, n) \geq 1$ for $m \neq n$

Informal description

For any two distinct integers $m$ and $n$, the distance between them is at least 1, i.e., $\text{dist}(m, n) \geq 1$.

Int.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 Integers into Reals

Informal description

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

Int.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 Integers into Reals

Informal description

The canonical embedding of the integers $\mathbb{Z}$ into the real numbers $\mathbb{R}$ is a closed embedding, meaning it is both a closed map and an embedding in the topological sense.

Int.instMetricSpace instance

: MetricSpace ℤ

Full source

instance : MetricSpace ℤ := Int.isUniformEmbedding_coe_real.comapMetricSpace _

The Metric Space Structure on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical metric space structure, which is induced from the metric space structure of the real numbers via the canonical embedding.

Int.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 Integers Equals Open Ball in Reals

Informal description

For any integer $x$ and real number $r$, the preimage of the open ball centered at $x$ with radius $r$ in $\mathbb{R}$ under the canonical embedding $\mathbb{Z} \to \mathbb{R}$ is equal to the open ball centered at $x$ with radius $r$ in $\mathbb{Z}$.

Int.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 Integers under Real Embedding Equals Integer Closed Ball

Informal description

For any integer $x$ and real number $r$, the preimage of the closed ball in $\mathbb{R}$ centered at $x$ with radius $r$ under the canonical embedding $\mathbb{Z} \hookrightarrow \mathbb{R}$ is equal to the closed ball in $\mathbb{Z}$ centered at $x$ with radius $r$.

Int.ball_eq_Ioo theorem

(x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉

Full source

theorem ball_eq_Ioo (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉ := by
  rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]

Open Ball in Integers as Floor-Ceiling Interval: $B(x, r) = (\lfloor x - r \rfloor, \lceil x + r \rceil)$

Informal description

For any integer $x$ and real number $r > 0$, the open ball $B(x, r)$ in the metric space of integers $\mathbb{Z}$ is equal to the open interval $(\lfloor x - r \rfloor, \lceil x + r \rceil)$ in $\mathbb{Z}$.

Int.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
  rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]

Closed Ball in Integers as Interval Between Ceiling and Floor

Informal description

For any integer $x$ and real number $r$, the closed ball in $\mathbb{Z}$ centered at $x$ with radius $r$ is equal to the closed interval of integers between $\lceil x - r \rceil$ and $\lfloor x + r \rfloor$. That is, $$ \{ z \in \mathbb{Z} \mid |z - x| \leq r \} = [\lceil x - r \rceil, \lfloor x + r \rfloor] \cap \mathbb{Z}. $$

Int.instProperSpace instance

: ProperSpace ℤ

Full source

instance : ProperSpace ℤ :=
  ⟨fun x r => by
    rw [closedBall_eq_Icc]
    exact (Set.finite_Icc _ _).isCompact⟩

Proper Metric Space Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a proper metric space, where the distance between two integers is induced from the standard metric on $\mathbb{R}$ via the canonical embedding.

Int.cobounded_eq theorem

: Bornology.cobounded ℤ = atBot ⊔ atTop

Full source

@[simp]
theorem cobounded_eq : Bornology.cobounded ℤ = atBotatBot ⊔ atTop := by
  simp_rw [← comap_dist_right_atTop (0 : ℤ), dist_eq', sub_zero,
    ← comap_abs_atTop, ← @Int.comap_cast_atTop ℝ, comap_comap]; rfl

Characterization of Cobounded Filter on Integers as Supremum of atBot and atTop

Informal description

The cobounded filter on the integers $\mathbb{Z}$ is equal to the supremum of the filters at negative infinity (`atBot`) and at positive infinity (`atTop$), i.e., $\text{cobounded}(\mathbb{Z}) = \text{atBot} \sqcup \text{atTop}$.

Int.cofinite_eq theorem

: (cofinite : Filter ℤ) = atBot ⊔ atTop

Full source

@[simp]
theorem cofinite_eq : (cofinite : Filter ℤ) = atBotatBot ⊔ atTop := by
  rw [← cocompact_eq_cofinite, cocompact_eq_atBot_atTop]

Cofinite Filter on Integers as Supremum of atBot and atTop

Informal description

The cofinite filter on the integers $\mathbb{Z}$ is equal to the supremum of the filters at negative infinity (`atBot`) and at positive infinity (`atTop$), i.e., $\text{cofinite}(\mathbb{Z}) = \text{atBot} \sqcup \text{atTop}$.