--- 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: