feat(Analysis/../Connected): balls are (pre)connected (leanprover-community#33514)

---
<!-- Your PR title will become the first line of the commit message.

In this box, the text above the `---` (if not empty) will be appended
to the commit message, and can be used to give additional context or
details. Please leave a blank newline before the `---`, otherwise GitHub
will format the text above it as a title.

For details on the "pull request lifecycle" in mathlib, please see:
https://leanprover-community.github.io/contribute/index.html

In particular, note that most reviewers will only notice your PR
if it passes the continuous integration checks.
Please ask for help on https://leanprover.zulipchat.com if needed.

When merging, all the commits will be squashed into a single commit
listing all co-authors.

Co-authors in the squash commit are gathered from two sources:

First, all authors of commits to this PR branch are included. Thus,
one way to add co-authors is to include at least one commit authored by
each co-author among the commits in the pull request. If necessary, you
may create empty commits to indicate co-authorship, using commands like so:

git commit --author="Author Name <author@email.com>" --allow-empty -m "add Author Name as coauthor"

Second, co-authors can also be listed in lines at the very bottom of
the commit message (that is, directly before the `---`) using the following format:


If you are moving or deleting declarations, please include these lines
at the bottom of the commit message (before the `---`, and also before
any "Co-authored-by" lines) using the following format:

Moves:
- Vector.* -> List.Vector.*
- ...

Deletions:
- Nat.bit1_add_bit1
- ...

Any other comments you want to keep out of the PR commit should go
below the `---`, and placed outside this HTML comment, or else they
will be invisible to reviewers.

If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]

-->

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Co-authored-by: Author Name <author@email.com>

Author: urkud

Mathlib/Analysis/Normed/Module/Connected.lean

@@ -31,7 +31,8 @@ public section
 assert_not_exists Subgroup.index Nat.divisors
 -- TODO assert_not_exists Cardinal
 
-open Convex Set Metric
+open Set Metric
+open scoped Convex ENNReal
 
 section TopologicalVectorSpace
 
@@ -135,39 +136,70 @@ section Ball
 
 namespace Metric
 
-theorem ball_contractible {x : E} {r : ℝ} (hr : 0 < r) :
+theorem contractibleSpace_ball {x : E} {r : ℝ} (hr : 0 < r) :
     ContractibleSpace (ball x r) :=
-  Convex.contractibleSpace (convex_ball _ _) (by simpa)
-
-theorem eball_contractible {x : E} {r : ENNReal} (hr : 0 < r) :
-    ContractibleSpace (Metric.eball x r) := by
-  cases r with
-  | top =>
-    rw [eball_top_eq_univ, (Homeomorph.Set.univ E).contractibleSpace_iff]
-    exact RealTopologicalVectorSpace.contractibleSpace
-  | coe r =>
-    rw [Metric.eball_coe]
-    apply ball_contractible
-    simpa using hr
+  (convex_ball _ _).contractibleSpace (by simpa)
+
+@[deprecated (since := "2026-02-02")]
+alias ball_contractible := contractibleSpace_ball
+
+theorem contractibleSpace_eball {x : E} {r : ℝ≥0∞} (hr : 0 < r) :
+    ContractibleSpace (eball x r) :=
+  (convex_eball _ _).contractibleSpace ⟨x, by simpa⟩
+
+@[deprecated (since := "2026-02-02")]
+alias eball_contractible := contractibleSpace_eball
+
+theorem contractibleSpace_closedBall {x : E} {r : ℝ} (hr : 0 ≤ r) :
+    ContractibleSpace (closedBall x r) :=
+  (convex_closedBall _ _).contractibleSpace (by simpa)
+
+instance contractibleSpace_closedEBall {x : E} {r : ℝ≥0∞} :
+    ContractibleSpace (closedEBall x r) :=
+  (convex_closedEBall _ _).contractibleSpace ⟨x, by simp⟩
 
 theorem isPathConnected_ball {x : E} {r : ℝ} (hr : 0 < r) :
-    IsPathConnected (ball x r) := by
-  rw [isPathConnected_iff_pathConnectedSpace]
-  exact @ContractibleSpace.instPathConnectedSpace _ _ (ball_contractible hr)
+    IsPathConnected (ball x r) :=
+  convex_ball _ _ |>.isPathConnected <| by simpa
+
+theorem isPathConnected_eball {x : E} {r : ℝ≥0∞} (hr : 0 < r) :
+    IsPathConnected (eball x r) :=
+  convex_eball _ _ |>.isPathConnected ⟨x, by simpa⟩
+
+theorem isPathConnected_closedBall {x : E} {r : ℝ} (hr : 0 ≤ r) :
+    IsPathConnected (closedBall x r) :=
+  convex_closedBall _ _ |>.isPathConnected ⟨x, by simpa⟩
 
-theorem isPathConnected_eball {x : E} {r : ENNReal} (hr : 0 < r) :
-    IsPathConnected (Metric.eball x r) := by
-  rw [isPathConnected_iff_pathConnectedSpace]
-  exact @ContractibleSpace.instPathConnectedSpace _ _ (eball_contractible hr)
+theorem isPathConnected_closedEBall {x : E} {r : ℝ≥0∞} :
+    IsPathConnected (closedEBall x r) :=
+  isPathConnected_iff_pathConnectedSpace.mpr inferInstance
+
+theorem isPreconnected_ball {x : E} {r : ℝ} : IsPreconnected (ball x r) :=
+  (convex_ball _ _).isPreconnected
+
+theorem isPreconnected_eball {x : E} {r : ℝ≥0∞} : IsPreconnected (eball x r) :=
+  (convex_eball _ _).isPreconnected
+
+theorem isPreconnected_closedBall {x : E} {r : ℝ} : IsPreconnected (closedBall x r) :=
+  (convex_closedBall _ _).isPreconnected
+
+theorem isPreconnected_closedEBall {x : E} {r : ℝ≥0∞} : IsPreconnected (closedEBall x r) :=
+  (convex_closedEBall _ _).isPreconnected
 
 theorem isConnected_ball {x : E} {r : ℝ} (hr : 0 < r) :
     IsConnected (ball x r) :=
   (isPathConnected_ball hr).isConnected
 
-theorem isConnected_eball {x : E} {r : ENNReal} (hr : 0 < r) :
-    IsConnected (Metric.eball x r) :=
+theorem isConnected_eball {x : E} {r : ℝ≥0∞} (hr : 0 < r) :
+    IsConnected (eball x r) :=
   (isPathConnected_eball hr).isConnected
 
+theorem isConnected_closedBall {x : E} {r : ℝ} (hr : 0 ≤ r) : IsConnected (closedBall x r) :=
+  ⟨⟨x, by simpa⟩, isPreconnected_closedBall⟩
+
+theorem isConnected_closedEBall {x : E} {r : ℝ≥0∞} : IsConnected (closedEBall x r) :=
+  ⟨⟨x, mem_closedEBall_self⟩, isPreconnected_closedEBall⟩
+
 end Metric
 
 end Ball

Mathlib/Analysis/Normed/Module/Convex.lean

@@ -60,12 +60,22 @@ theorem convexOn_dist (z : E) (hs : Convex ℝ s) : ConvexOn ℝ s fun z' => dis
 theorem convexOn_univ_dist (z : E) : ConvexOn ℝ univ fun z' => dist z' z :=
   convexOn_dist z convex_univ
 
-theorem convex_ball (a : E) (r : ℝ) : Convex ℝ (Metric.ball a r) := by
+theorem convex_ball (a : E) (r : ℝ) : Convex ℝ (ball a r) := by
   simpa only [Metric.ball, sep_univ] using (convexOn_univ_dist a).convex_lt r
 
+theorem convex_eball (a : E) (r : ENNReal) : Convex ℝ (eball a r) := by
+  cases r with
+  | top => simp [convex_univ]
+  | coe r => simp [eball_coe, convex_ball]
+
 theorem convex_closedBall (a : E) (r : ℝ) : Convex ℝ (Metric.closedBall a r) := by
   simpa only [Metric.closedBall, sep_univ] using (convexOn_univ_dist a).convex_le r
 
+theorem convex_closedEBall (a : E) (r : ENNReal) : Convex ℝ (closedEBall a r) := by
+  cases r with
+  | top => simp [convex_univ]
+  | coe r => simp [closedEBall_coe, convex_closedBall]
+
 open Pointwise in
 theorem convexHull_sphere_eq_closedBall {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
     [Nontrivial F] (x : F) {r : ℝ} (hr : 0 ≤ r) :