diff -r c6e9c7d140ff -r 65cd285f6b9c src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Jun 21 22:57:40 2017 +0200
+++ b/src/HOL/Topological_Spaces.thy	Thu Jun 22 10:50:18 2017 +0200
@@ -662,6 +662,17 @@
   shows   "eventually P (at_right a)"
   using assms unfolding eventually_at_topological by (intro exI[of _ "{..<b}"]) auto
 
+lemma eventually_filtercomap_nhds:
+  "eventually P (filtercomap f (nhds x)) \<longleftrightarrow> (\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x. f x \<in> S \<longrightarrow> P x))"
+  unfolding eventually_filtercomap eventually_nhds by auto
+
+lemma eventually_filtercomap_at_topological:
+  "eventually P (filtercomap f (at A within B)) \<longleftrightarrow> 
+     (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))" (is "?lhs = ?rhs")
+  unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal 
+          eventually_filtercomap_nhds eventually_principal by blast
+    
+
 
 subsubsection \<open>Tendsto\<close>