[STATEMENT]
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")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually P (filtercomap f (at A within B)) = (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))
[PROOF STEP]
unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal 
          eventually_filtercomap_nhds eventually_principal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<longrightarrow> x \<in> f -` (B - {A}) \<longrightarrow> P x)) = (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))
[PROOF STEP]
by blast