--- a/src/HOL/Real_Vector_Spaces.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Feb 23 13:27:19 2018 +0000
@@ -1768,6 +1768,10 @@
for a :: "'a :: metric_space"
by (auto simp: eventually_at_filter eventually_nhds_metric)
+lemma frequently_at: "frequently P (at a within S) \<longleftrightarrow> (\<forall>d>0. \<exists>x\<in>S. x \<noteq> a \<and> dist x a < d \<and> P x)"
+ for a :: "'a :: metric_space"
+ unfolding frequently_def eventually_at by auto
+
lemma eventually_at_le: "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a \<le> d \<longrightarrow> P x)"
for a :: "'a::metric_space"
apply (simp only: eventually_at_filter eventually_nhds_metric)