Topology on the integers

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

@[implicit_reducible]

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

theorem Int.isClosedEmbedding_coe_real : Topology.IsClosedEmbedding Int.cast

@[implicit_reducible]

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 ℤ

instance Int.instIsOrderBornology : IsOrderBornology ℤ

@[deprecated IsOrderBornology.cobounded_eq (since := "2026-04-07")]

theorem Int.cobounded_eq {α : Type u_1} [Bornology α] [Nonempty α] [LinearOrder α] [IsOrderBornology α] [NoMaxOrder α] [NoMinOrder α] : Bornology.cobounded α = Filter.atBot ⊔ Filter.atTop

Alias of IsOrderBornology.cobounded_eq.

@[simp]

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