mathlib3 documentation


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 .

@[protected, instance]
theorem nat.dist_eq (x y : ) :
@[simp, norm_cast]
theorem nat.pairwise_one_le_dist  :
pairwise (λ (m n : ), 1 has_dist.dist m n)
@[protected, instance]
@[protected, instance]