src/HOL/Analysis/FPS_Convergence.thy

--- a/src/HOL/Analysis/FPS_Convergence.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -61,6 +61,9 @@
 lemma open_eball [simp, intro]: "open (eball z r)" 
   by (cases r) auto
 
+lemma connected_eball [intro]: "connected (eball (z :: 'a :: real_normed_vector) r)"
+  by (cases r) auto
+
 
 subsection \<open>Basic properties of convergent power series\<close>