Topology on the natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

@[protected, instance]

def nat.has_dist :

has_dist ℕ

Equations

nat.has_dist = {dist := λ (x y : ℕ), has_dist.dist ↑x ↑y}

source

theorem nat.dist_eq (x y : ℕ) :

has_dist.dist x y = |↑x - ↑y|

source

theorem nat.dist_coe_int (x y : ℕ) :

has_dist.dist ↑x ↑y = has_dist.dist x y

source

@[simp, norm_cast]

theorem nat.dist_cast_real (x y : ℕ) :

has_dist.dist ↑x ↑y = has_dist.dist x y

source

theorem nat.pairwise_one_le_dist :

pairwise (λ (m n : ℕ), 1 ≤ has_dist.dist m n)

source

theorem nat.uniform_embedding_coe_real :

uniform_embedding coe

source

theorem nat.closed_embedding_coe_real :

closed_embedding coe

source

@[protected, instance]

def nat.metric_space :

metric_space ℕ

Equations

nat.metric_space = uniform_embedding.comap_metric_space coe nat.uniform_embedding_coe_real

source

theorem nat.preimage_ball (x : ℕ) (r : ℝ) :

coe ⁻¹' metric.ball ↑x r = metric.ball x r

source

theorem nat.preimage_closed_ball (x : ℕ) (r : ℝ) :

coe ⁻¹' metric.closed_ball ↑x r = metric.closed_ball x r

source

theorem nat.closed_ball_eq_Icc (x : ℕ) (r : ℝ) :

metric.closed_ball x r = set.Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

source

@[protected, instance]

def nat.proper_space :

proper_space ℕ

source

@[protected, instance]

def nat.noncompact_space :

noncompact_space ℕ