refactor(topology/metric_space/basic): rename closed_ball_Icc (#8790)

* rename `closed_ball_Icc` to `real.closed_ball_eq`;
* add `real.ball_eq`, `int.ball_eq`, `int.closed_ball_eq`,
  `int.preimage_ball`, `int.preimage_closed_ball`.

Author: urkud

src/number_theory/liouville/basic.lean

@@ -146,7 +146,7 @@ begin
   { exact λ a, one_le_pow_of_one_le ((le_add_iff_nonneg_left 1).mpr a.cast_nonneg) _ },
   -- 2: the polynomial `fR` is Lipschitz at `α` -- as its derivative continuous;
   { rw mul_comm,
-    rw closed_ball_Icc at hy,
+    rw real.closed_ball_eq at hy,
     -- apply the Mean Value Theorem: the bound on the derivative comes from differentiability.
     refine convex.norm_image_sub_le_of_norm_deriv_le (λ _ _, fR.differentiable_at)
       (λ y h, by { rw fR.deriv, exact hM _ h }) (convex_Icc _ _) hy (mem_Icc_iff_abs_le.mp _),

src/topology/instances/real.lean

@@ -29,6 +29,8 @@ theorem rat.dist_eq (x y : ℚ) : dist x y = abs (x - y) := rfl
 
 @[norm_cast, simp] lemma rat.dist_cast (x y : ℚ) : dist (x : ℝ) y = dist x y := rfl
 
+namespace int
+
 section low_prio
 -- we want to ignore this instance for the next declaration
 local attribute [instance, priority 10] int.uniform_space
@@ -46,21 +48,33 @@ begin
 end
 end low_prio
 
-theorem int.dist_eq (x y : ℤ) : dist x y = abs (x - y) := rfl
+theorem dist_eq (x y : ℤ) : dist x y = abs (x - y) := rfl
 
-@[norm_cast, simp] theorem int.dist_cast_real (x y : ℤ) : dist (x : ℝ) y = dist x y := rfl
+@[norm_cast, simp] theorem dist_cast_real (x y : ℤ) : dist (x : ℝ) y = dist x y := rfl
 
-@[norm_cast, simp] theorem int.dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y :=
+@[norm_cast, simp] theorem dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y :=
 by rw [← int.dist_cast_real, ← rat.dist_cast]; congr' 1; norm_cast
 
+theorem preimage_ball (x : ℤ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball x r := rfl
+
+theorem preimage_closed_ball (x : ℤ) (r : ℝ) :
+  coe ⁻¹' (closed_ball (x : ℝ) r) = closed_ball x r := rfl
+
+theorem ball_eq (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉ :=
+by rw [← preimage_ball, real.ball_eq, preimage_Ioo]
+
+theorem closed_ball_eq (x : ℤ) (r : ℝ) : closed_ball x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋ :=
+by rw [← preimage_closed_ball, real.closed_ball_eq, preimage_Icc]
+
 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],
+    rw closed_ball_eq,
+    exact (set.Icc_ℤ_finite _ _).is_compact,
   end ⟩
 
+end int
+
 theorem uniform_continuous_of_rat : uniform_continuous (coe : ℚ → ℝ) :=
 uniform_continuous_comap
 
@@ -111,7 +125,7 @@ instance : order_topology ℚ :=
 induced_order_topology _ (λ x y, rat.cast_lt) (@exists_rat_btwn _ _ _)
 
 instance : proper_space ℝ :=
-{ compact_ball := λx r, by { rw closed_ball_Icc, apply is_compact_Icc } }
+{ compact_ball := λx r, by { rw real.closed_ball_eq, apply is_compact_Icc } }
 
 instance : second_countable_topology ℝ := second_countable_of_proper
 
@@ -264,7 +278,7 @@ lemma real.bounded_iff_bdd_below_bdd_above {s : set ℝ} : bounded s ↔ bdd_bel
 ⟨begin
   assume bdd,
   rcases (bounded_iff_subset_ball 0).1 bdd with ⟨r, hr⟩, -- hr : s ⊆ closed_ball 0 r
-  rw closed_ball_Icc at hr, -- hr : s ⊆ Icc (0 - r) (0 + r)
+  rw real.closed_ball_eq at hr, -- hr : s ⊆ Icc (0 - r) (0 + r)
   exact ⟨bdd_below_Icc.mono hr, bdd_above_Icc.mono hr⟩
 end,
 begin

src/topology/metric_space/basic.lean

@@ -951,7 +951,11 @@ instance : order_topology ℝ :=
 order_topology_of_nhds_abs $ λ x,
   by simp only [nhds_basis_ball.eq_binfi, ball, real.dist_eq, abs_sub_comm]
 
-lemma closed_ball_Icc {x r : ℝ} : closed_ball x r = Icc (x-r) (x+r) :=
+lemma real.ball_eq (x r : ℝ) : ball x r = Ioo (x - r) (x + r) :=
+set.ext $ λ y, by rw [mem_ball, dist_comm, real.dist_eq,
+  abs_sub_lt_iff, mem_Ioo, ← sub_lt_iff_lt_add', sub_lt]
+
+lemma real.closed_ball_eq {x r : ℝ} : closed_ball x r = Icc (x - r) (x + r) :=
 by ext y; rw [mem_closed_ball, dist_comm, real.dist_eq,
   abs_sub_le_iff, mem_Icc, ← sub_le_iff_le_add', sub_le]
 
@@ -1844,7 +1848,7 @@ begin
   { rw ← bounded_iff_subset_ball,
     exact hs.bounded },
   refine ⟨(coe ⁻¹' closed_ball (0:ℝ) r)ᶜ, _, _⟩,
-  { simp [mem_cofinite, closed_ball_Icc, set.Icc_ℤ_finite] },
+  { simp [mem_cofinite, real.closed_ball_eq, set.Icc_ℤ_finite] },
   { rw ← compl_subset_compl at hr,
     intros y hy,
     exact hr hy }