Topology on the natural numbers #
The structure of a metric space on ℕ
is introduced in this file, induced from ℝ
.
theorem
Nat.preimage_closedBall
(x : ℕ)
(r : ℝ)
:
Nat.cast ⁻¹' Metric.closedBall (↑x) r = Metric.closedBall x r
Mathlib.Topology.Instances.Nat
The structure of a metric space on ℕ
is introduced in this file, induced from ℝ
.