Topology on the integers #
The structure of a metric space on ℤ
is introduced in this file, induced from ℝ
.
@[deprecated Int.isUniformEmbedding_coe_real]
Alias of Int.isUniformEmbedding_coe_real
.
theorem
Int.preimage_closedBall
(x : ℤ)
(r : ℝ)
:
Int.cast ⁻¹' Metric.closedBall (↑x) r = Metric.closedBall x r
@[deprecated cocompact_eq_atBot_atTop]
theorem
Int.cocompact_eq
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMaxOrder α]
[NoMinOrder α]
[OrderClosedTopology α]
[CompactIccSpace α]
:
Filter.cocompact α = Filter.atBot ⊔ Filter.atTop
Alias of cocompact_eq_atBot_atTop
.