diff -r e6edd47f1483 -r 3f5b2745d659 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Feb 25 15:02:54 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Feb 25 16:17:20 2014 +0000
@@ -1706,6 +1706,11 @@
   unfolding continuous_on_open_invariant
   by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
 
+corollary continuous_imp_open_vimage:
+  assumes "continuous_on s f" "open s" "open B" "f -` B \<subseteq> s"
+    shows "open (f -` B)"
+by (metis assms continuous_on_open_vimage le_iff_inf)
+
 lemma continuous_on_closed_invariant:
   "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
 proof -