Topology on the natural numbers

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

noncomputable instance Nat.instDistNat : Dist ℕ

Equations

• Nat.instDistNat = { 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.uniformEmbedding_coe_real : UniformEmbedding Nat.cast

theorem Nat.closedEmbedding_coe_real : ClosedEmbedding Nat.cast

instance Nat.instMetricSpaceNat : MetricSpace ℕ

Equations

• Nat.instMetricSpaceNat = UniformEmbedding.comapMetricSpace Nat.cast Nat.uniformEmbedding_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.instProperSpaceNatToPseudoMetricSpaceInstMetricSpaceNat : ProperSpace ℕ

Equations

• Nat.instProperSpaceNatToPseudoMetricSpaceInstMetricSpaceNat = Nat.instProperSpaceNatToPseudoMetricSpaceInstMetricSpaceNat.proof_1

instance Nat.instNoncompactSpaceNatInstTopologicalSpaceNat : NoncompactSpace ℕ

Equations

• Nat.instNoncompactSpaceNatInstTopologicalSpaceNat = Nat.instNoncompactSpaceNatInstTopologicalSpaceNat.proof_1