mathlib documentation

topology.instances.int

Topology on the integers #

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

@[protected, instance]
noncomputable def int.has_dist  :
Equations
theorem int.dist_eq (x y : ) :
dist x y = |x - y|
@[simp, norm_cast]
theorem int.dist_cast_real (x y : ) :
dist x y = dist x y
theorem int.pairwise_one_le_dist  :
pairwise (λ (m n : ), 1 dist m n)
theorem int.ball_eq_Ioo (x : ) (r : ) :
@[protected, instance]