diff -r ed38f9a834d8 -r 05a2b3b20664 src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 05 16:03:23 2017 +0000
+++ b/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 05 16:37:49 2017 +0000
@@ -1388,4 +1388,127 @@
    shows "g1 x = g2 x"
 using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv by blast
 
+
+lemma covering_space_locally:
+  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes loc: "locally \<phi> C" and cov: "covering_space C p S"
+      and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
+    shows "locally \<psi> S"
+proof -
+  have "locally \<psi> (p ` C)"
+    apply (rule locally_open_map_image [OF loc])
+    using cov covering_space_imp_continuous apply blast
+    using cov covering_space_imp_surjective covering_space_open_map apply blast
+    by (simp add: pim)
+  then show ?thesis
+    using covering_space_imp_surjective [OF cov] by metis
+qed
+
+
+proposition covering_space_locally_eq:
+  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes cov: "covering_space C p S"
+      and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
+      and qim: "\<And>q U. \<lbrakk>U \<subseteq> S; continuous_on U q; \<psi> U\<rbrakk> \<Longrightarrow> \<phi>(q ` U)"
+    shows "locally \<psi> S \<longleftrightarrow> locally \<phi> C"
+         (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  show ?rhs
+  proof (rule locallyI)
+    fix V x
+    assume V: "openin (subtopology euclidean C) V" and "x \<in> V"
+    have "p x \<in> p ` C"
+      by (metis IntE V \<open>x \<in> V\<close> imageI openin_open)
+    then obtain T \<V> where "p x \<in> T"
+                      and opeT: "openin (subtopology euclidean S) T"
+                      and veq: "\<Union>\<V> = {x \<in> C. p x \<in> T}"
+                      and ope: "\<forall>U\<in>\<V>. openin (subtopology euclidean C) U"
+                      and hom: "\<forall>U\<in>\<V>. \<exists>q. homeomorphism U T p q"
+      using cov unfolding covering_space_def by (blast intro: that)
+    have "x \<in> \<Union>\<V>"
+      using V veq \<open>p x \<in> T\<close> \<open>x \<in> V\<close> openin_imp_subset by fastforce
+    then obtain U where "x \<in> U" "U \<in> \<V>"
+      by blast
+    then obtain q where opeU: "openin (subtopology euclidean C) U" and q: "homeomorphism U T p q"
+      using ope hom by blast
+    with V have "openin (subtopology euclidean C) (U \<inter> V)"
+      by blast
+    then have UV: "openin (subtopology euclidean S) (p ` (U \<inter> V))"
+      using cov covering_space_open_map by blast
+    obtain W W' where opeW: "openin (subtopology euclidean S) W" and "\<psi> W'" "p x \<in> W" "W \<subseteq> W'" and W'sub: "W' \<subseteq> p ` (U \<inter> V)"
+      using locallyE [OF L UV] \<open>x \<in> U\<close> \<open>x \<in> V\<close> by blast
+    then have "W \<subseteq> T"
+      by (metis Int_lower1 q homeomorphism_image1 image_Int_subset order_trans)
+    show "\<exists>U Z. openin (subtopology euclidean C) U \<and>
+                 \<phi> Z \<and> x \<in> U \<and> U \<subseteq> Z \<and> Z \<subseteq> V"
+    proof (intro exI conjI)
+      have "openin (subtopology euclidean T) W"
+        by (meson opeW opeT openin_imp_subset openin_subset_trans \<open>W \<subseteq> T\<close>)
+      then have "openin (subtopology euclidean U) (q ` W)"
+        by (meson homeomorphism_imp_open_map homeomorphism_symD q)
+      then show "openin (subtopology euclidean C) (q ` W)"
+        using opeU openin_trans by blast
+      show "\<phi> (q ` W')"
+        by (metis (mono_tags, lifting) Int_subset_iff UV W'sub \<open>\<psi> W'\<close> continuous_on_subset dual_order.trans homeomorphism_def image_Int_subset openin_imp_subset q qim)
+      show "x \<in> q ` W"
+        by (metis \<open>p x \<in> W\<close> \<open>x \<in> U\<close> homeomorphism_def imageI q)
+      show "q ` W \<subseteq> q ` W'"
+        using \<open>W \<subseteq> W'\<close> by blast
+      have "W' \<subseteq> p ` V"
+        using W'sub by blast
+      then show "q ` W' \<subseteq> V"
+        using W'sub homeomorphism_apply1 [OF q] by auto
+      qed
+  qed
+next
+  assume ?rhs
+  then show ?lhs
+    using cov covering_space_locally pim by blast
+qed
+
+lemma covering_space_locally_compact_eq:
+  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes "covering_space C p S"
+  shows "locally compact S \<longleftrightarrow> locally compact C"
+  apply (rule covering_space_locally_eq [OF assms])
+   apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
+  using compact_continuous_image by blast
+
+lemma covering_space_locally_connected_eq:
+  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes "covering_space C p S"
+    shows "locally connected S \<longleftrightarrow> locally connected C"
+  apply (rule covering_space_locally_eq [OF assms])
+   apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
+  using connected_continuous_image by blast
+
+lemma covering_space_locally_path_connected_eq:
+  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes "covering_space C p S"
+    shows "locally path_connected S \<longleftrightarrow> locally path_connected C"
+  apply (rule covering_space_locally_eq [OF assms])
+   apply (meson path_connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
+  using path_connected_continuous_image by blast
+
+
+lemma covering_space_locally_compact:
+  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes "locally compact C" "covering_space C p S"
+  shows "locally compact S"
+  using assms covering_space_locally_compact_eq by blast
+
+
+lemma covering_space_locally_connected:
+  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes "locally connected C" "covering_space C p S"
+  shows "locally connected S"
+  using assms covering_space_locally_connected_eq by blast
+
+lemma covering_space_locally_path_connected:
+  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes "locally path_connected C" "covering_space C p S"
+  shows "locally path_connected S"
+  using assms covering_space_locally_path_connected_eq by blast
+
 end