chore(topology/{metric_space,instances/real}): cleanup (#10577)

* merge `real.ball_eq` and `real.ball_eq_Ioo` into `real.ball_eq_Ioo`;
* merge `real.closed_ball_eq` and `real.closed_ball_eq_Icc` into `real.closed_ball_eq_Icc`;
* add missing `real.Icc_eq_closed_ball`;
* generalize lemmas about `*bounded_Ixx` so that they work for (indexed) products of conditionally complete linear orders.

src/analysis/seminorm.lean

@@ -526,7 +526,7 @@ begin
   { simpa only [s', f, set.mem_preimage, one_smul] },
   obtain ⟨ε, hε₀, hε⟩ := (metric.nhds_basis_closed_ball.1 _).1
     (is_open_iff_mem_nhds.1 hs' 1 one_mem),
-  rw real.closed_ball_eq at hε,
+  rw real.closed_ball_eq_Icc at hε,
   have hε₁ : 0 < 1 + ε := hε₀.trans (lt_one_add ε),
   have : (1 + ε)⁻¹ < 1,
   { rw inv_lt_one_iff,

src/measure_theory/measure/lebesgue.lean

@@ -67,11 +67,11 @@ ennreal.eq_top_of_forall_nnreal_le $ λ r,
 
 @[simp] lemma volume_ball (a r : ℝ) :
   volume (metric.ball a r) = of_real (2 * r) :=
-by rw [ball_eq, volume_Ioo, ← sub_add, add_sub_cancel', two_mul]
+by rw [ball_eq_Ioo, volume_Ioo, ← sub_add, add_sub_cancel', two_mul]
 
 @[simp] lemma volume_closed_ball (a r : ℝ) :
   volume (metric.closed_ball a r) = of_real (2 * r) :=
-by rw [closed_ball_eq, volume_Icc, ← sub_add, add_sub_cancel', two_mul]
+by rw [closed_ball_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel', two_mul]
 
 @[simp] lemma volume_emetric_ball (a : ℝ) (r : ℝ≥0∞) :
   volume (emetric.ball a r) = 2 * r :=

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 real.closed_ball_eq at hy,
+    rw real.closed_ball_eq_Icc 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

@@ -85,16 +85,16 @@ theorem preimage_ball (x : ℤ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball
 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 ball_eq_Ioo (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉ :=
+by rw [← preimage_ball, real.ball_eq_Ioo, 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]
+theorem closed_ball_eq_Icc (x : ℤ) (r : ℝ) : closed_ball x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋ :=
+by rw [← preimage_closed_ball, real.closed_ball_eq_Icc, preimage_Icc]
 
 instance : proper_space ℤ :=
 ⟨ begin
     intros x r,
-    rw closed_ball_eq,
+    rw closed_ball_eq_Icc,
     exact (set.finite_Icc _ _).is_compact,
   end ⟩
 
@@ -144,7 +144,7 @@ instance : order_topology ℚ :=
 induced_order_topology _ (λ x y, rat.cast_lt) (@exists_rat_btwn _ _ _)
 
 instance : proper_space ℝ :=
-{ is_compact_closed_ball := λx r, by { rw real.closed_ball_eq, apply is_compact_Icc } }
+{ is_compact_closed_ball := λx r, by { rw real.closed_ball_eq_Icc, apply is_compact_Icc } }
 
 instance : second_countable_topology ℝ := second_countable_of_proper
 
@@ -239,15 +239,6 @@ real.continuous_mul.comp ((rat.continuous_coe_real.prod_map rat.continuous_coe_r
 instance : topological_ring ℚ :=
 { continuous_mul := rat.continuous_mul, ..rat.topological_add_group }
 
-theorem real.ball_eq_Ioo (x ε : ℝ) : ball x ε = Ioo (x - ε) (x + ε) :=
-set.ext $ λ y, by rw [mem_ball, real.dist_eq,
-  abs_sub_lt_iff, sub_lt_iff_lt_add', and_comm, sub_lt]; refl
-
-theorem real.Ioo_eq_ball (x y : ℝ) : Ioo x y = ball ((x + y) / 2) ((y - x) / 2) :=
-by rw [real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add,
-  add_sub_cancel', add_self_div_two, ← add_div,
-  add_assoc, add_sub_cancel'_right, add_self_div_two]
-
 instance : complete_space ℝ :=
 begin
   apply complete_of_cauchy_seq_tendsto,
@@ -294,14 +285,10 @@ 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 real.closed_ball_eq at hr, -- hr : s ⊆ Icc (0 - r) (0 + r)
+  rw real.closed_ball_eq_Icc at hr, -- hr : s ⊆ Icc (0 - r) (0 + r)
   exact ⟨bdd_below_Icc.mono hr, bdd_above_Icc.mono hr⟩
 end,
-begin
-  intro h,
-  rcases bdd_below_bdd_above_iff_subset_Icc.1 h with ⟨m, M, I : s ⊆ Icc m M⟩,
-  exact (bounded_Icc m M).mono I
-end⟩
+λ h, bounded_of_bdd_above_of_bdd_below h.2 h.1⟩
 
 lemma real.subset_Icc_Inf_Sup_of_bounded {s : set ℝ} (h : bounded s) :
   s ⊆ Icc (Inf s) (Sup s) :=

src/topology/metric_space/basic.lean

@@ -1020,17 +1020,27 @@ 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 real.ball_eq (x r : ℝ) : ball x r = Ioo (x - r) (x + r) :=
+lemma real.ball_eq_Ioo (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) :=
+lemma real.closed_ball_eq_Icc {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]
 
+theorem real.Ioo_eq_ball (x y : ℝ) : Ioo x y = ball ((x + y) / 2) ((y - x) / 2) :=
+by rw [real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add,
+  add_sub_cancel', add_self_div_two, ← add_div,
+  add_assoc, add_sub_cancel'_right, add_self_div_two]
+
+theorem real.Icc_eq_closed_ball (x y : ℝ) : Icc x y = closed_ball ((x + y) / 2) ((y - x) / 2) :=
+by rw [real.closed_ball_eq_Icc, ← sub_div, add_comm, ← sub_add,
+  add_sub_cancel', add_self_div_two, ← add_div,
+  add_assoc, add_sub_cancel'_right, add_self_div_two]
+
 section metric_ordered
 
-variables [conditionally_complete_linear_order α] [order_topology α]
+variables [preorder α] [compact_Icc_space α]
 
 lemma totally_bounded_Icc (a b : α) : totally_bounded (Icc a b) :=
 is_compact_Icc.totally_bounded
@@ -1794,7 +1804,7 @@ lemma compact_space_iff_bounded_univ [proper_space α] : compact_space α ↔ bo
 
 section conditionally_complete_linear_order
 
-variables [conditionally_complete_linear_order α] [order_topology α]
+variables [preorder α] [compact_Icc_space α]
 
 lemma bounded_Icc (a b : α) : bounded (Icc a b) :=
 (totally_bounded_Icc a b).bounded
@@ -1996,7 +2006,7 @@ begin
   refine tendsto_cocompact_of_tendsto_dist_comp_at_top (0 : ℝ) _,
   simp only [filter.tendsto_at_top, eventually_cofinite, not_le, ← mem_ball],
   change ∀ r : ℝ, finite (coe ⁻¹' (ball (0 : ℝ) r)),
-  simp [real.ball_eq, set.finite_Ioo],
+  simp [real.ball_eq_Ioo, set.finite_Ioo],
 end
 
 end int