A couple of additional lemmas

--- 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

--- a/src/HOL/Analysis/Sparse_In.thy	Wed Feb 12 08:48:15 2025 +0100
+++ b/src/HOL/Analysis/Sparse_In.thy	Wed Feb 12 16:27:24 2025 +0000
@@ -90,6 +90,10 @@
   by (metis Diff_Diff_Int Diff_cancel Diff_eq_empty_iff Diff_subset 
       closedin_def double_diff openin_open_eq topspace_euclidean_subtopology)
 
+lemma sparse_in_UNIV_imp_closed: "X sparse_in UNIV \<Longrightarrow> closed X"
+  by (simp add: Compl_eq_Diff_UNIV closed_open open_diff_sparse_pts)
+
+
 lemma sparse_imp_countable:
   fixes D::"'a ::euclidean_space set"
   assumes  "open D" "pts sparse_in D"
@@ -196,10 +200,8 @@
 
 lemma eventually_cosparse_imp_eventually_at:
   "eventually P (cosparse A) \<Longrightarrow> x \<in> A \<Longrightarrow> eventually P (at x within B)"
-  unfolding eventually_cosparse sparse_in_def
-  apply (auto simp: islimpt_conv_frequently_at frequently_def)
-   apply (metis UNIV_I eventually_at_topological)
-  done
+  unfolding eventually_cosparse sparse_in_def islimpt_def eventually_at_topological 
+  by fastforce
 
 lemma eventually_in_cosparse:
   assumes "A \<subseteq> X" "open A"
@@ -227,5 +229,4 @@
 lemma cosparse_eq_bot_iff' [simp]: "cosparse (A :: 'a :: perfect_space set) = bot \<longleftrightarrow> A = {}"
   by (auto simp: cosparse_eq_bot_iff not_open_singleton)
 
-
 end
\ No newline at end of file