Topology on the integers

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

instance Int.instDist : Dist ℤ

Equations

• Int.instDist = { dist := fun (x y : ℤ) => dist ↑x ↑y }

theorem Int.dist_eq (x y : ℤ) : dist x y = |↑x - ↑y|

theorem Int.dist_eq' (m n : ℤ) : dist m n = ↑|m - n|

@[simp]

theorem Int.dist_cast_real (x y : ℤ) : dist ↑x ↑y = dist x y

theorem Int.pairwise_one_le_dist : Pairwise fun (m n : ℤ) => 1 ≤ dist m n

theorem Int.isUniformEmbedding_coe_real : IsUniformEmbedding Int.cast

@[deprecated Int.isUniformEmbedding_coe_real (since := "2024-10-01")]

theorem Int.uniformEmbedding_coe_real : IsUniformEmbedding Int.cast

Alias of Int.isUniformEmbedding_coe_real.

theorem Int.isClosedEmbedding_coe_real : Topology.IsClosedEmbedding Int.cast

@[deprecated Int.isClosedEmbedding_coe_real (since := "2024-10-20")]

theorem Int.closedEmbedding_coe_real : Topology.IsClosedEmbedding Int.cast

Alias of Int.isClosedEmbedding_coe_real.

instance Int.instMetricSpace : MetricSpace ℤ

Equations

• Int.instMetricSpace = IsUniformEmbedding.comapMetricSpace Int.cast Int.isUniformEmbedding_coe_real

theorem Int.preimage_ball (x : ℤ) (r : ℝ) : Int.cast ⁻¹' Metric.ball (↑x) r = Metric.ball x r

theorem Int.preimage_closedBall (x : ℤ) (r : ℝ) : Int.cast ⁻¹' Metric.closedBall (↑x) r = Metric.closedBall x r

theorem Int.ball_eq_Ioo (x : ℤ) (r : ℝ) : Metric.ball x r = Set.Ioo ⌊↑x - r⌋ ⌈↑x + r⌉

theorem Int.closedBall_eq_Icc (x : ℤ) (r : ℝ) : Metric.closedBall x r = Set.Icc ⌈↑x - r⌉ ⌊↑x + r⌋

instance Int.instProperSpace : ProperSpace ℤ

@[simp]

theorem Int.cobounded_eq : Bornology.cobounded ℤ = Filter.atBot ⊔ Filter.atTop

@[simp]

theorem Int.cofinite_eq : Filter.cofinite = Filter.atBot ⊔ Filter.atTop