--- a/src/HOL/Analysis/Isolated.thy	Wed Feb 12 08:48:15 2025 +0100
+++ b/src/HOL/Analysis/Isolated.thy	Wed Feb 12 16:27:24 2025 +0000
@@ -1,5 +1,5 @@
 theory Isolated
-  imports "HOL-Analysis.Elementary_Metric_Spaces"
+  imports "Elementary_Metric_Spaces" "Sparse_In"
 
 begin
 
@@ -324,4 +324,10 @@
   finally show ?thesis .
 qed
 
+lemma uniform_discrete_imp_sparse:
+  assumes "uniform_discrete X"
+  shows   "X sparse_in A"
+  using assms unfolding uniform_discrete_def sparse_in_ball_def
+  by (auto simp: discrete_imp_not_islimpt)
+
 end