Topology on the natural numbers

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

@[implicit_reducible]

noncomputable instance Nat.instDist : Dist ℕ

theorem Nat.dist_eq (x y : ℕ) : Dist.dist x y = |↑x - ↑y|

theorem Nat.dist_coe_int (x y : ℕ) : Dist.dist ↑x ↑y = Dist.dist x y

@[simp]

theorem Nat.dist_cast_real (x y : ℕ) : Dist.dist ↑x ↑y = Dist.dist x y

theorem Nat.pairwise_one_le_dist : Pairwise fun (m n : ℕ) => 1 ≤ Dist.dist m n

theorem Nat.isUniformEmbedding_coe_real : IsUniformEmbedding Nat.cast

theorem Nat.isClosedEmbedding_coe_real : Topology.IsClosedEmbedding Nat.cast

@[implicit_reducible]

instance Nat.instMetricSpace : MetricSpace ℕ

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

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

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

instance Nat.instProperSpace : ProperSpace ℕ

instance Nat.instIsOrderBornology : IsOrderBornology ℕ

instance Nat.instNoncompactSpace : NoncompactSpace ℕ