diff -r 5e82015fa879 -r f2d327275065 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Sun Mar 24 20:31:53 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue Mar 26 17:01:36 2019 +0000
@@ -1609,6 +1609,8 @@
   qed
 qed (auto simp: continuous_map_on_empty)
 
+declare continuous_map_const [THEN iffD2, continuous_intros]
+
 lemma continuous_map_compose:
   assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
   shows "continuous_map X X'' (g \<circ> f)"
@@ -3773,6 +3775,13 @@
   shows "closedin (top_of_set S) (S \<inter> f -` T)"
   using assms continuous_on_closed by blast
 
+lemma continuous_map_subtopology_eu [simp]:
+  "continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
+  apply safe
+  apply (metis continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
+  apply (simp add: continuous_map_closedin_preimage_eq image_subset_iff)
+  by (metis (no_types, hide_lams) continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
+
 subsection%unimportant \<open>Half-global and completely global cases\<close>
 
 lemma continuous_openin_preimage_gen: