Topology on the integers #

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 int.has_dist :

has_dist ℤ

Equations

int.has_dist = {dist := λ (x y : ℤ), has_dist.dist ↑x ↑y}

source

theorem int.dist_eq (x y : ℤ) :

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

source

@[simp, norm_cast]

theorem int.dist_cast_real (x y : ℤ) :

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

source

theorem int.pairwise_one_le_dist :

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

source

theorem int.uniform_embedding_coe_real :

uniform_embedding coe

source

theorem int.closed_embedding_coe_real :

closed_embedding coe

source

@[protected, instance]

def int.metric_space :

metric_space ℤ

Equations

int.metric_space = uniform_embedding.comap_metric_space coe int.uniform_embedding_coe_real

source

theorem int.preimage_ball (x : ℤ) (r : ℝ) :

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

source

theorem int.preimage_closed_ball (x : ℤ) (r : ℝ) :

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

source

theorem int.ball_eq_Ioo (x : ℤ) (r : ℝ) :

metric.ball x r = set.Ioo ⌊↑x - r⌋ ⌈↑x + r⌉

source

theorem int.closed_ball_eq_Icc (x : ℤ) (r : ℝ) :

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

source

@[protected, instance]

def int.proper_space :

proper_space ℤ

source

@[simp]

theorem int.cocompact_eq :

filter.cocompact ℤ = filter.at_bot ⊔ filter.at_top

source

@[simp]

theorem int.cofinite_eq :

filter.cofinite = filter.at_bot ⊔ filter.at_top