chore(topology): rename compact_ball to is_compact_closed_ball (#9337)

The old name didn't follow the naming convention at all, which made it hard to discover.

src/analysis/calculus/specific_functions.lean

@@ -406,7 +406,7 @@ lemma closure_support_eq : closure (support f) = euclidean.closed_ball c f.R :=
 by rw [f.support_eq, euclidean.closure_ball _ f.R_pos]
 
 lemma compact_closure_support : is_compact (closure (support f)) :=
-by { rw f.closure_support_eq, exact euclidean.compact_ball }
+by { rw f.closure_support_eq, exact euclidean.is_compact_closed_ball }
 
 lemma eventually_eq_one_of_mem_ball (h : x ∈ euclidean.ball c f.r) :
   f =ᶠ[𝓝 x] 1 :=

src/analysis/normed_space/euclidean_dist.lean

@@ -61,14 +61,14 @@ lemma closed_ball_eq_image (x : E) (r : ℝ) :
   closed_ball x r = to_euclidean.symm '' metric.closed_ball (to_euclidean x) r :=
 by rw [to_euclidean.image_symm_eq_preimage, closed_ball_eq_preimage]
 
-lemma compact_ball {x : E} {r : ℝ} : is_compact (closed_ball x r) :=
+lemma is_compact_closed_ball {x : E} {r : ℝ} : is_compact (closed_ball x r) :=
 begin
   rw closed_ball_eq_image,
-  exact (proper_space.compact_ball _ _).image to_euclidean.symm.continuous
+  exact (proper_space.is_compact_closed_ball _ _).image to_euclidean.symm.continuous
 end
 
 lemma is_closed_closed_ball {x : E} {r : ℝ} : is_closed (closed_ball x r) :=
-compact_ball.is_closed
+is_compact_closed_ball.is_closed
 
 lemma closure_ball (x : E) {r : ℝ} (h : 0 < r) : closure (ball x r) = closed_ball x r :=
 by rw [ball_eq_preimage, ← to_euclidean.preimage_closure, closure_ball (to_euclidean x) h,

src/geometry/manifold/bump_function.lean

@@ -176,7 +176,7 @@ lemma nonempty_support : (support f).nonempty := ⟨c, f.c_mem_support⟩
 
 lemma compact_symm_image_closed_ball :
   is_compact ((ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I)) :=
-(compact_ball.inter_right I.closed_range).image_of_continuous_on $
+(is_compact_closed_ball.inter_right I.closed_range).image_of_continuous_on $
   (ext_chart_at_continuous_on_symm _ _).mono f.closed_ball_subset
 
 /-- Given a smooth bump function `f : smooth_bump_function I c`, the closed ball of radius `f.R` is

src/topology/instances/real.lean

@@ -121,7 +121,7 @@ instance : order_topology ℚ :=
 induced_order_topology _ (λ x y, rat.cast_lt) (@exists_rat_btwn _ _ _)
 
 instance : proper_space ℝ :=
-{ compact_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, apply is_compact_Icc } }
 
 instance : second_countable_topology ℝ := second_countable_of_proper
 

src/topology/metric_space/basic.lean

@@ -1419,12 +1419,12 @@ open metric
 
 /-- A pseudometric space is proper if all closed balls are compact. -/
 class proper_space (α : Type u) [pseudo_metric_space α] : Prop :=
-(compact_ball : ∀x:α, ∀r, is_compact (closed_ball x r))
+(is_compact_closed_ball : ∀x:α, ∀r, is_compact (closed_ball x r))
 
 /-- In a proper pseudometric space, all spheres are compact. -/
 lemma is_compact_sphere {α : Type*} [pseudo_metric_space α] [proper_space α] (x : α) (r : ℝ) :
   is_compact (sphere x r) :=
-compact_of_is_closed_subset (proper_space.compact_ball x r) is_closed_sphere
+compact_of_is_closed_subset (proper_space.is_compact_closed_ball x r) is_closed_sphere
   sphere_subset_closed_ball
 
 /-- In a proper pseudometric space, any sphere is a `compact_space` when considered as a subtype. -/
@@ -1441,15 +1441,16 @@ begin
   -- add an instance for `sigma_compact_space`.
   suffices : sigma_compact_space α, by exactI emetric.second_countable_of_sigma_compact α,
   rcases em (nonempty α) with ⟨⟨x⟩⟩|hn,
-  { exact ⟨⟨λ n, closed_ball x n, λ n, proper_space.compact_ball _ _,
+  { exact ⟨⟨λ n, closed_ball x n, λ n, proper_space.is_compact_closed_ball _ _,
       Union_closed_ball_nat _⟩⟩ },
   { exact ⟨⟨λ n, ∅, λ n, is_compact_empty, Union_eq_univ_iff.2 $ λ x, (hn ⟨x⟩).elim⟩⟩ }
 end
 
 lemma tendsto_dist_right_cocompact_at_top [proper_space α] (x : α) :
   tendsto (λ y, dist y x) (cocompact α) at_top :=
 (has_basis_cocompact.tendsto_iff at_top_basis).2 $ λ r hr,
-  ⟨closed_ball x r, proper_space.compact_ball x r, λ y hy, (not_le.1 $ mt mem_closed_ball.2 hy).le⟩
+  ⟨closed_ball x r, proper_space.is_compact_closed_ball x r, 
+    λ y hy, (not_le.1 $ mt mem_closed_ball.2 hy).le⟩
 
 lemma tendsto_dist_left_cocompact_at_top [proper_space α] (x : α) :
   tendsto (dist x) (cocompact α) at_top :=
@@ -1482,7 +1483,7 @@ instance proper_of_compact [compact_space α] : proper_space α :=
 instance locally_compact_of_proper [proper_space α] :
   locally_compact_space α :=
 locally_compact_space_of_has_basis (λ x, nhds_basis_closed_ball) $
-  λ x ε ε0, proper_space.compact_ball _ _
+  λ x ε ε0, proper_space.is_compact_closed_ball _ _
 
 /-- A proper space is complete -/
 @[priority 100] -- see Note [lower instance priority]
@@ -1495,7 +1496,7 @@ instance complete_of_proper [proper_space α] : complete_space α :=
     (metric.cauchy_iff.1 hf).2 1 zero_lt_one,
   rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩,
   have : closed_ball x 1 ∈ f := mem_of_superset t_fset (λ y yt, (ht y x yt xt).le),
-  rcases (compact_iff_totally_bounded_complete.1 (proper_space.compact_ball x 1)).2 f hf
+  rcases (compact_iff_totally_bounded_complete.1 (proper_space.is_compact_closed_ball x 1)).2 f hf
     (le_principal_iff.2 this) with ⟨y, -, hy⟩,
   exact ⟨y, hy⟩
 end⟩
@@ -1507,7 +1508,7 @@ begin
   refine proper_space_of_compact_closed_ball_of_le 0 (λx r hr, _),
   rw closed_ball_pi _ hr,
   apply is_compact_univ_pi (λb, _),
-  apply (h b).compact_ball
+  apply (h b).is_compact_closed_ball
 end
 
 variables [proper_space α] {x : α} {r : ℝ} {s : set α}
@@ -1520,7 +1521,7 @@ begin
   unfreezingI { rcases eq_empty_or_nonempty s with rfl|hne },
   { exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩ },
   have : is_compact s,
-    from compact_of_is_closed_subset (proper_space.compact_ball x r) hs
+    from compact_of_is_closed_subset (proper_space.is_compact_closed_ball x r) hs
       (subset.trans h ball_subset_closed_ball),
   obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closed_ball x (dist y x),
     from this.exists_forall_ge hne (continuous_id.dist continuous_const).continuous_on,
@@ -1696,7 +1697,7 @@ begin
   unfreezingI { rcases eq_empty_or_nonempty s with (rfl|⟨x, hx⟩) },
   { exact is_compact_empty },
   { rcases hb.subset_ball x with ⟨r, hr⟩,
-    exact compact_of_is_closed_subset (proper_space.compact_ball x r) hc hr }
+    exact compact_of_is_closed_subset (proper_space.is_compact_closed_ball x r) hc hr }
 end
 
 /-- The Heine–Borel theorem: