feat(topology/instances/real, topology/metric_space/basic, algebra/floor): integers are a proper space (#6437)

The metric space `ℤ` is a proper space.  Also, under the coercion from `ℤ` to `ℝ`, inverse images of compact sets are finite.

The key point for both facts is to express the inverse image of an `ℝ`-interval under the coercion as an appropriate `ℤ`-interval, using floor or ceiling of the endpoints -- I provide these facts as simp-lemmas.

Indirectly related discussion:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Finiteness.20of.20balls.20in.20the.20integers

Author: hrmacbeth

src/algebra/floor.lean

@@ -7,6 +7,7 @@ import tactic.linarith
 import tactic.abel
 import algebra.ordered_group
 import data.set.intervals.basic
+
 /-!
 # Floor and Ceil
 
@@ -289,3 +290,35 @@ lt_of_le_of_lt (le_nat_ceil x) (by exact_mod_cast h)
 
 lemma le_of_nat_ceil_le {x : α} {n : ℕ} (h : nat_ceil x ≤ n) : x ≤ n :=
 le_trans (le_nat_ceil x) (by exact_mod_cast h)
+
+namespace int
+
+@[simp] lemma preimage_Ioo {x y : α} :
+  ((coe : ℤ → α) ⁻¹' (set.Ioo x y)) = set.Ioo (floor x) (ceil y) :=
+by { ext, simp [floor_lt, lt_ceil] }
+
+@[simp] lemma preimage_Ico {x y : α} :
+  ((coe : ℤ → α) ⁻¹' (set.Ico x y)) = set.Ico (ceil x) (ceil y) :=
+by { ext, simp [ceil_le, lt_ceil] }
+
+@[simp] lemma preimage_Ioc {x y : α} :
+  ((coe : ℤ → α) ⁻¹' (set.Ioc x y)) = set.Ioc (floor x) (floor y) :=
+by { ext, simp [floor_lt, le_floor] }
+
+@[simp] lemma preimage_Icc {x y : α} :
+  ((coe : ℤ → α) ⁻¹' (set.Icc x y)) = set.Icc (ceil x) (floor y) :=
+by { ext, simp [ceil_le, le_floor] }
+
+@[simp] lemma preimage_Ioi {x : α} : ((coe : ℤ → α) ⁻¹' (set.Ioi x)) = set.Ioi (floor x) :=
+by { ext, simp [floor_lt] }
+
+@[simp] lemma preimage_Ici {x : α} : ((coe : ℤ → α) ⁻¹' (set.Ici x)) = set.Ici (ceil x) :=
+by { ext, simp [ceil_le] }
+
+@[simp] lemma preimage_Iio {x : α} : ((coe : ℤ → α) ⁻¹' (set.Iio x)) = set.Iio (ceil x) :=
+by { ext, simp [lt_ceil] }
+
+@[simp] lemma preimage_Iic {x : α} : ((coe : ℤ → α) ⁻¹' (set.Iic x)) = set.Iic (floor x) :=
+by { ext, simp [le_floor] }
+
+end int

src/topology/instances/real.lean

@@ -52,6 +52,14 @@ theorem int.dist_eq (x y : ℤ) : dist x y = abs (x - y) := rfl
 @[norm_cast, simp] theorem int.dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y :=
 by rw [← int.dist_cast_real, ← rat.dist_cast]; congr' 1; norm_cast
 
+instance : proper_space ℤ :=
+⟨ begin
+    intros x r,
+    apply set.finite.is_compact,
+    have : closed_ball x r = coe ⁻¹' (closed_ball (x:ℝ) r) := rfl,
+    simp [this, closed_ball_Icc, set.Icc_ℤ_finite],
+  end ⟩
+
 theorem uniform_continuous_of_rat : uniform_continuous (coe : ℚ → ℝ) :=
 uniform_continuous_comap
 

src/topology/metric_space/basic.lean

@@ -11,6 +11,7 @@ topological spaces. For example:
 -/
 import topology.metric_space.emetric_space
 import topology.algebra.ordered
+import data.fintype.intervals
 
 open set filter classical topological_space
 noncomputable theory
@@ -1700,3 +1701,23 @@ le_trans (diam_mono ball_subset_closed_ball bounded_closed_ball) (diam_closed_ba
 end diam
 
 end metric
+
+namespace int
+open metric
+
+/-- Under the coercion from `ℤ` to `ℝ`, inverse images of compact sets are finite. -/
+lemma tendsto_coe_cofinite : tendsto (coe : ℤ → ℝ) cofinite (cocompact ℝ) :=
+begin
+  simp only [filter.has_basis_cocompact.tendsto_right_iff, eventually_iff_exists_mem],
+  intros s hs,
+  obtain ⟨r, hr⟩ : ∃ r, s ⊆ closed_ball (0:ℝ) r,
+  { rw ← bounded_iff_subset_ball,
+    exact hs.bounded },
+  refine ⟨(coe ⁻¹' closed_ball (0:ℝ) r)ᶜ, _, _⟩,
+  { simp [mem_cofinite, closed_ball_Icc, set.Icc_ℤ_finite] },
+  { rw ← compl_subset_compl at hr,
+    intros y hy,
+    exact hr hy }
+end
+
+end int