Topology on the natural numbers #
The structure of a metric space on ℕ
is introduced in this file, induced from ℝ
.
Equations
- Nat.instDist = { dist := fun (x y : ℕ) => dist ↑x ↑y }
The structure of a metric space on ℕ
is introduced in this file, induced from ℝ
.