Topology on the positive natural numbers

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

instance PNat.instMetricSpace : MetricSpace ℕ+

Equations

• PNat.instMetricSpace = inferInstanceAs (MetricSpace { n : ℕ // 0 < n })

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

@[simp]

theorem PNat.dist_coe (x y : ℕ+) : dist ↑x ↑y = dist x y

theorem PNat.isUniformEmbedding_coe : IsUniformEmbedding val

@[deprecated PNat.isUniformEmbedding_coe (since := "2024-10-01")]

theorem PNat.uniformEmbedding_coe : IsUniformEmbedding val

Alias of PNat.isUniformEmbedding_coe.

instance PNat.instDiscreteTopology : DiscreteTopology ℕ+

instance PNat.instProperSpace : ProperSpace ℕ+

instance PNat.instNoncompactSpace : NoncompactSpace ℕ+