Topology on the positive natural numbers

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

@[implicit_reducible]

instance PNat.instMetricSpace : MetricSpace ℕ+

Equations

• One or more equations did not get rendered due to their size.

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

instance PNat.instDiscreteTopology : DiscreteTopology ℕ+

instance PNat.instProperSpace : ProperSpace ℕ+

instance PNat.instNoncompactSpace : NoncompactSpace ℕ+