Topology on the natural numbers

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

noncomputable instance Nat.instDist : Dist ℕ

Equations

• Nat.instDist = { dist := fun (x y : ℕ) => dist ↑x ↑y }

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

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

@[simp]

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

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

theorem Nat.isUniformEmbedding_coe_real : IsUniformEmbedding Nat.cast

@[deprecated Nat.isUniformEmbedding_coe_real]

theorem Nat.uniformEmbedding_coe_real : IsUniformEmbedding Nat.cast

Alias of Nat.isUniformEmbedding_coe_real.

theorem Nat.isClosedEmbedding_coe_real : Topology.IsClosedEmbedding Nat.cast

@[deprecated Nat.isClosedEmbedding_coe_real]

theorem Nat.closedEmbedding_coe_real : Topology.IsClosedEmbedding Nat.cast

Alias of Nat.isClosedEmbedding_coe_real.

instance Nat.instMetricSpace : MetricSpace ℕ

Equations

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

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 ℕ

Equations

• Nat.instProperSpace = ⋯

instance Nat.instNoncompactSpace : NoncompactSpace ℕ

Equations

• Nat.instNoncompactSpace = ⋯