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
@[deprecated Nat.isUniformEmbedding_coe_real (since := "2024-10-01")]

Alias of Nat.isUniformEmbedding_coe_real.

@[deprecated Nat.isClosedEmbedding_coe_real (since := "2024-10-20")]

Alias of Nat.isClosedEmbedding_coe_real.