Documentation

Mathlib.Topology.Instances.PNat

Topology on the positive natural numbers #

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

source
instance PNat.instMetricSpace :
MetricSpace ℕ+
Equations
    source
    theorem PNat.dist_eq (x y : ℕ+) :
    dist x y = |↑↑x - ↑↑y|
    source
    @[simp]
    theorem PNat.dist_coe (x y : ℕ+) :
    dist ↑x ↑y = dist x y
    source
    theorem PNat.isUniformEmbedding_coe :
    IsUniformEmbedding val
    source
    instance PNat.instDiscreteTopology :
    DiscreteTopology ℕ+
    source
    instance PNat.instProperSpace :
    ProperSpace ℕ+
    source
    instance PNat.instNoncompactSpace :
    NoncompactSpace ℕ+