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 PNat.val

@[deprecated PNat.isUniformEmbedding_coe]

theorem PNat.uniformEmbedding_coe : IsUniformEmbedding PNat.val

Alias of PNat.isUniformEmbedding_coe.

instance PNat.instDiscreteTopology : DiscreteTopology ℕ+

Equations

• PNat.instDiscreteTopology = ⋯

instance PNat.instProperSpace : ProperSpace ℕ+

Equations

• PNat.instProperSpace = ⋯

instance PNat.instNoncompactSpace : NoncompactSpace ℕ+

Equations

• PNat.instNoncompactSpace = ⋯