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.uniformEmbedding_coe_real : UniformEmbedding Int.cast

theorem Int.closedEmbedding_coe_real : ClosedEmbedding Int.cast

instance Int.instMetricSpace : MetricSpace ℤ

Equations

• Int.instMetricSpace = UniformEmbedding.comapMetricSpace Int.cast Int.uniformEmbedding_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 ℤ

Equations

• Int.instProperSpace = ⋯

@[simp]

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

@[deprecated cocompact_eq_atBot_atTop]

theorem Int.cocompact_eq {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [NoMaxOrder α] [NoMinOrder α] [OrderClosedTopology α] [CompactIccSpace α] : Filter.cocompact α = Filter.atBot ⊔ Filter.atTop

Alias of cocompact_eq_atBot_atTop.

@[simp]

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