--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Apr 15 15:17:25 2025 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Apr 15 17:38:20 2025 +0200
@@ -366,6 +366,12 @@
for x :: "'a::{perfect_space,metric_space}"
using islimpt_UNIV [of x] by (simp add: islimpt_approachable)
+
+lemma pointed_ball_nonempty:
+ assumes "r > 0"
+ shows "ball x r - {x :: 'a :: {perfect_space, metric_space}} \<noteq> {}"
+ using perfect_choose_dist[of r x] assms by (auto simp: ball_def dist_commute)
+
lemma cball_eq_sing:
fixes x :: "'a::{metric_space,perfect_space}"
shows "cball x e = {x} \<longleftrightarrow> e = 0"