Documentation

Mathlib.Topology.Instances.Nat

Topology on the natural numbers #

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

noncomputable instance Nat.instDist :
Equations
theorem Nat.dist_eq (x : ) (y : ) :
dist x y = |x - y|
theorem Nat.dist_coe_int (x : ) (y : ) :
dist x y = dist x y
@[simp]
theorem Nat.dist_cast_real (x : ) (y : ) :
dist x y = dist x y
theorem Nat.pairwise_one_le_dist :
Pairwise fun (m n : ) => 1 dist m n
theorem Nat.preimage_ball (x : ) (r : ) :
Nat.cast ⁻¹' Metric.ball (x) r = Metric.ball x r