# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1553695706 0
# Node ID cf7150ab107561a6931ed813c8c892c114d56d16
# Parent  3fd083253a1cc5bcb560a1d79fc717dcc8b6da9e
more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.

diff -r 3fd083253a1c -r cf7150ab1075 src/HOL/Analysis/Abstract_Euclidean_Space.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Wed Mar 27 14:08:26 2019 +0000
@@ -0,0 +1,345 @@
+(*  Author:  LCP, ported from HOL Light
+*)
+
+section\<open>Euclidean space and n-spheres, as subtopologies of n-dimensional space\<close>
+
+theory Abstract_Euclidean_Space
+imports Homotopy Locally T1_Spaces
+begin
+
+subsection \<open>Euclidean spaces as abstract topologies\<close>
+
+definition Euclidean_space :: "nat \<Rightarrow> (nat \<Rightarrow> real) topology"
+  where "Euclidean_space n \<equiv> subtopology (powertop_real UNIV) {x. \<forall>i\<ge>n. x i = 0}"
+
+lemma topspace_Euclidean_space:
+   "topspace(Euclidean_space n) = {x. \<forall>i\<ge>n. x i = 0}"
+  by (simp add: Euclidean_space_def)
+
+lemma nonempty_Euclidean_space: "topspace(Euclidean_space n) \<noteq> {}"
+  by (force simp: topspace_Euclidean_space)
+
+lemma subset_Euclidean_space [simp]:
+   "topspace(Euclidean_space m) \<subseteq> topspace(Euclidean_space n) \<longleftrightarrow> m \<le> n"
+  apply (simp add: topspace_Euclidean_space subset_iff, safe)
+   apply (drule_tac x="(\<lambda>i. if i < m then 1 else 0)" in spec)
+   apply auto
+  using not_less by fastforce
+
+lemma topspace_Euclidean_space_alt:
+  "topspace(Euclidean_space n) = (\<Inter>i \<in> {n..}. {x. x \<in> topspace(powertop_real UNIV) \<and> x i \<in> {0}})"
+  by (auto simp: topspace_Euclidean_space)
+
+lemma closedin_Euclidean_space:
+  "closedin (powertop_real UNIV) (topspace(Euclidean_space n))"
+proof -
+  have "closedin (powertop_real UNIV) {x. x i = 0}" if "n \<le> i" for i
+  proof -
+    have "closedin (powertop_real UNIV) {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}"
+    proof (rule closedin_continuous_map_preimage)
+      show "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. x i)"
+        by (metis UNIV_I continuous_map_product_coordinates)
+      show "closedin euclideanreal {0}"
+        by simp
+    qed
+    then show ?thesis
+      by auto
+  qed
+  then show ?thesis
+    unfolding topspace_Euclidean_space_alt
+    by force
+qed
+
+lemma closedin_Euclidean_imp_closed: "closedin (Euclidean_space m) S \<Longrightarrow> closed S"
+  by (metis Euclidean_space_def closed_closedin closedin_Euclidean_space closedin_closed_subtopology euclidean_product_topology topspace_Euclidean_space)
+
+lemma closedin_Euclidean_space_iff:
+  "closedin (Euclidean_space m) S \<longleftrightarrow> closed S \<and> S \<subseteq> topspace (Euclidean_space m)"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    using closedin_closed_subtopology topspace_Euclidean_space
+    by (fastforce simp: topspace_Euclidean_space_alt closedin_Euclidean_imp_closed)
+  show "?rhs \<Longrightarrow> ?lhs"
+  apply (simp add: closedin_subtopology Euclidean_space_def)
+    by (metis (no_types) closed_closedin euclidean_product_topology inf.orderE)
+qed
+
+lemma continuous_map_componentwise_Euclidean_space:
+  "continuous_map X (Euclidean_space n) (\<lambda>x i. if i < n then f x i else 0) \<longleftrightarrow>
+   (\<forall>i < n. continuous_map X euclideanreal (\<lambda>x. f x i))"
+proof -
+  have *: "continuous_map X euclideanreal (\<lambda>x. if k < n then f x k else 0)"
+    if "\<And>i. i<n \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)" for k
+    by (intro continuous_intros that)
+  show ?thesis
+    unfolding Euclidean_space_def continuous_map_in_subtopology
+    by (fastforce simp: continuous_map_componentwise_UNIV * elim: continuous_map_eq)
+qed
+
+lemma continuous_map_Euclidean_space_add [continuous_intros]:
+   "\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
+    \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i + g x i)"
+  unfolding Euclidean_space_def continuous_map_in_subtopology
+  by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_real_add)
+
+lemma continuous_map_Euclidean_space_diff [continuous_intros]:
+   "\<lbrakk>continuous_map X (Euclidean_space n) f; continuous_map X (Euclidean_space n) g\<rbrakk>
+    \<Longrightarrow> continuous_map X (Euclidean_space n) (\<lambda>x i. f x i - g x i)"
+  unfolding Euclidean_space_def continuous_map_in_subtopology
+  by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_real_diff)
+
+lemma homeomorphic_Euclidean_space_product_topology:
+  "Euclidean_space n homeomorphic_space product_topology (\<lambda>i. euclideanreal) {..<n}"
+proof -
+  have cm: "continuous_map (product_topology (\<lambda>i. euclideanreal) {..<n})
+          euclideanreal (\<lambda>x. if k < n then x k else 0)" for k
+    by (auto intro: continuous_map_if continuous_map_product_projection)
+  show ?thesis
+    unfolding homeomorphic_space_def homeomorphic_maps_def
+    apply (rule_tac x="\<lambda>f. restrict f {..<n}" in exI)
+    apply (rule_tac x="\<lambda>f i. if i < n then f i else 0" in exI)
+    apply (simp add: Euclidean_space_def topspace_subtopology continuous_map_in_subtopology)
+    apply (intro conjI continuous_map_from_subtopology)
+       apply (force simp: continuous_map_componentwise cm intro: continuous_map_product_projection)+
+    done
+qed
+
+lemma contractible_Euclidean_space [simp]: "contractible_space (Euclidean_space n)"
+  using homeomorphic_Euclidean_space_product_topology contractible_space_euclideanreal
+    contractible_space_product_topology homeomorphic_space_contractibility by blast
+
+lemma path_connected_Euclidean_space: "path_connected_space (Euclidean_space n)"
+  by (simp add: contractible_imp_path_connected_space)
+
+lemma connected_Euclidean_space: "connected_space (Euclidean_space n)"
+  by (simp add: contractible_Euclidean_space contractible_imp_connected_space)
+
+lemma locally_path_connected_Euclidean_space:
+   "locally_path_connected_space (Euclidean_space n)"
+  apply (simp add: homeomorphic_locally_path_connected_space [OF homeomorphic_Euclidean_space_product_topology [of n]]
+                   locally_path_connected_space_product_topology)
+  using locally_path_connected_space_euclideanreal by auto
+
+lemma compact_Euclidean_space:
+   "compact_space (Euclidean_space n) \<longleftrightarrow> n = 0"
+  by (auto simp: homeomorphic_compact_space [OF homeomorphic_Euclidean_space_product_topology] compact_space_product_topology)
+
+subsection\<open>n-dimensional spheres\<close>
+
+definition nsphere where
+ "nsphere n \<equiv> subtopology (Euclidean_space (Suc n)) { x. (\<Sum>i\<le>n. x i ^ 2) = 1 }"
+
+lemma nsphere:
+   "nsphere n = subtopology (powertop_real UNIV)
+                            {x. (\<Sum>i\<le>n. x i ^ 2) = 1 \<and> (\<forall>i>n. x i = 0)}"
+  by (simp add: nsphere_def Euclidean_space_def subtopology_subtopology Suc_le_eq Collect_conj_eq Int_commute)
+
+lemma continuous_map_nsphere_projection: "continuous_map (nsphere n) euclideanreal (\<lambda>x. x k)"
+  unfolding nsphere
+  by (blast intro: continuous_map_from_subtopology [OF continuous_map_product_projection])
+
+lemma in_topspace_nsphere: "(\<lambda>n. if n = 0 then 1 else 0) \<in> topspace (nsphere n)"
+  by (simp add: nsphere_def topspace_Euclidean_space power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
+
+lemma nonempty_nsphere [simp]: "~ (topspace(nsphere n) = {})"
+  using in_topspace_nsphere by auto
+
+lemma subtopology_nsphere_equator:
+  "subtopology (nsphere (Suc n)) {x. x(Suc n) = 0} = nsphere n"
+proof -
+  have "({x. (\<Sum>i\<le>n. (x i)\<^sup>2) + (x (Suc n))\<^sup>2 = 1 \<and> (\<forall>i>Suc n. x i = 0)} \<inter> {x. x (Suc n) = 0})
+      = {x. (\<Sum>i\<le>n. (x i)\<^sup>2) = 1 \<and> (\<forall>i>n. x i = (0::real))}"
+    using Suc_lessI [of n] by (fastforce simp: set_eq_iff)
+  then show ?thesis
+    by (simp add: nsphere subtopology_subtopology)
+qed
+
+lemma continuous_map_nsphere_reflection:
+  "continuous_map (nsphere n) (nsphere n) (\<lambda>x i. if i = k then -x i else x i)"
+proof -
+  have cm: "continuous_map (powertop_real UNIV)
+           euclideanreal (\<lambda>x. if j = k then - x j else x j)" for j
+  proof (cases "j=k")
+    case True
+    then show ?thesis
+      by simp (metis UNIV_I continuous_map_product_projection continuous_map_real_minus)
+  next
+    case False
+    then show ?thesis
+      by (auto intro: continuous_map_product_projection)
+  qed
+  have eq: "(if i = k then x k * x k else x i * x i) = x i * x i" for i and x :: "nat \<Rightarrow> real"
+    by simp
+  show ?thesis
+    apply (simp add: nsphere continuous_map_in_subtopology continuous_map_componentwise_UNIV
+        continuous_map_from_subtopology  cm topspace_subtopology)
+    apply (intro conjI allI impI continuous_intros continuous_map_from_subtopology continuous_map_product_projection)
+      apply (auto simp: power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] eq cong: if_cong)
+    done
+qed
+
+
+proposition contractible_space_upper_hemisphere:
+  assumes "k \<le> n"
+  shows "contractible_space(subtopology (nsphere n) {x. x k \<ge> 0})"
+proof -
+  define p:: "nat \<Rightarrow> real" where "p \<equiv> \<lambda>i. if i = k then 1 else 0"
+  have "p \<in> topspace(nsphere n)"
+    using assms
+    by (simp add: nsphere topspace_subtopology p_def power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
+  let ?g = "\<lambda>x i. x i / sqrt(\<Sum>j\<le>n. x j ^ 2)"
+  let ?h = "\<lambda>(t,q) i. (1 - t) * q i + t * p i"
+  let ?Y = "subtopology (Euclidean_space (Suc n)) {x. 0 \<le> x k \<and> (\<exists>i\<le>n. x i \<noteq> 0)}"
+  have "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (nsphere n) {x. 0 \<le> x k}))
+                       (subtopology (nsphere n) {x. 0 \<le> x k}) (?g \<circ> ?h)"
+  proof (rule continuous_map_compose)
+    have *: "\<lbrakk>0 \<le> b k; (\<Sum>i\<le>n. (b i)\<^sup>2) = 1; \<forall>i>n. b i = 0; 0 \<le> a; a \<le> 1\<rbrakk>
+           \<Longrightarrow> \<exists>i. (i = k \<longrightarrow> (1 - a) * b k + a \<noteq> 0) \<and>
+                   (i \<noteq> k \<longrightarrow> i \<le> n \<and> a \<noteq> 1 \<and> b i \<noteq> 0)" for a::real and b
+      apply (cases "a \<noteq> 1 \<and> b k = 0"; simp)
+       apply (metis (no_types, lifting) atMost_iff sum.neutral zero_power2)
+      by (metis add.commute add_le_same_cancel2 diff_ge_0_iff_ge diff_zero less_eq_real_def mult_eq_0_iff mult_nonneg_nonneg not_le numeral_One zero_neq_numeral)
+    show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (nsphere n) {x. 0 \<le> x k})) ?Y ?h"
+      using assms
+      apply (auto simp: * nsphere topspace_subtopology continuous_map_componentwise_UNIV
+               prod_topology_subtopology subtopology_subtopology case_prod_unfold
+               continuous_map_in_subtopology Euclidean_space_def p_def if_distrib [where f = "\<lambda>x. _ * x"] cong: if_cong)
+      apply (intro continuous_map_prod_snd continuous_intros continuous_map_from_subtopology)
+        apply auto
+      done
+  next
+    have 1: "\<And>x i. \<lbrakk> i \<le> n; x i \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>i\<le>n. (x i / sqrt (\<Sum>j\<le>n. (x j)\<^sup>2))\<^sup>2) = 1"
+      by (force simp: sum_nonneg sum_nonneg_eq_0_iff divide_simps simp flip: sum_divide_distrib)
+    have cm: "continuous_map ?Y (nsphere n) (\<lambda>x i. x i / sqrt (\<Sum>j\<le>n. (x j)\<^sup>2))"
+      unfolding Euclidean_space_def nsphere subtopology_subtopology continuous_map_in_subtopology
+    proof (intro continuous_intros conjI)
+      show "continuous_map
+               (subtopology (powertop_real UNIV) ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> {x. 0 \<le> x k \<and> (\<exists>i\<le>n. x i \<noteq> 0)}))
+               (powertop_real UNIV) (\<lambda>x i. x i / sqrt (\<Sum>j\<le>n. (x j)\<^sup>2))"
+        unfolding continuous_map_componentwise
+        by (intro continuous_intros conjI ballI) (auto simp: sum_nonneg_eq_0_iff)
+    qed (auto simp: 1)
+    show "continuous_map ?Y (subtopology (nsphere n) {x. 0 \<le> x k}) (\<lambda>x i. x i / sqrt (\<Sum>j\<le>n. (x j)\<^sup>2))"
+      by (force simp: cm sum_nonneg continuous_map_in_subtopology if_distrib [where f = "\<lambda>x. _ * x"] cong: if_cong)
+  qed
+  moreover have "(?g \<circ> ?h) (0, x) = x"
+    if "x \<in> topspace (subtopology (nsphere n) {x. 0 \<le> x k})" for x
+    using that
+    by (simp add: assms topspace_subtopology nsphere)
+  moreover
+  have "(?g \<circ> ?h) (1, x) = p"
+    if "x \<in> topspace (subtopology (nsphere n) {x. 0 \<le> x k})" for x
+    by (force simp: assms p_def power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
+  ultimately
+  show ?thesis
+    apply (simp add: contractible_space_def homotopic_with)
+    apply (rule_tac x=p in exI)
+    apply (rule_tac x="?g \<circ> ?h" in exI, force)
+    done
+qed
+
+
+corollary contractible_space_lower_hemisphere:
+  assumes "k \<le> n"
+  shows "contractible_space(subtopology (nsphere n) {x. x k \<le> 0})"
+proof -
+  have "contractible_space (subtopology (nsphere n) {x. 0 \<le> x k}) = ?thesis"
+  proof (rule homeomorphic_space_contractibility)
+    show "subtopology (nsphere n) {x. 0 \<le> x k} homeomorphic_space subtopology (nsphere n) {x. x k \<le> 0}"
+      unfolding homeomorphic_space_def homeomorphic_maps_def
+      apply (rule_tac x="\<lambda>x i. if i = k then -(x i) else x i" in exI)+
+      apply (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology
+                  continuous_map_nsphere_reflection)
+      done
+  qed
+  then show ?thesis
+    using contractible_space_upper_hemisphere [OF assms] by metis
+qed
+
+
+proposition nullhomotopic_nonsurjective_sphere_map:
+  assumes f: "continuous_map (nsphere p) (nsphere p) f"
+    and fim: "f ` (topspace(nsphere p)) \<noteq> topspace(nsphere p)"
+  obtains a where "homotopic_with (\<lambda>x. True) (nsphere p) (nsphere p) f (\<lambda>x. a)"
+proof -
+  obtain a where a: "a \<in> topspace(nsphere p)" "a \<notin> f ` (topspace(nsphere p))"
+    using fim continuous_map_image_subset_topspace f by blast
+  then have a1: "(\<Sum>i\<le>p. (a i)\<^sup>2) = 1" and a0: "\<And>i. i > p \<Longrightarrow> a i = 0"
+    by (simp_all add: nsphere)
+  have f1: "(\<Sum>j\<le>p. (f x j)\<^sup>2) = 1" if "x \<in> topspace (nsphere p)" for x
+  proof -
+    have "f x \<in> topspace (nsphere p)"
+      using continuous_map_image_subset_topspace f that by blast
+    then show ?thesis
+      by (simp add: nsphere)
+  qed
+  show thesis
+  proof
+    let ?g = "\<lambda>x i. x i / sqrt(\<Sum>j\<le>p. x j ^ 2)"
+    let ?h = "\<lambda>(t,x) i. (1 - t) * f x i - t * a i"
+    let ?Y = "subtopology (Euclidean_space(Suc p)) (- {\<lambda>i. 0})"
+    let ?T01 = "top_of_set {0..1::real}"
+    have 1: "continuous_map (prod_topology ?T01 (nsphere p)) (nsphere p) (?g \<circ> ?h)"
+    proof (rule continuous_map_compose)
+      have "continuous_map (prod_topology ?T01 (nsphere p)) euclideanreal ((\<lambda>x. f x k) \<circ> snd)" for k
+        unfolding nsphere
+        apply (simp add: continuous_map_of_snd)
+        apply (rule continuous_map_compose [of _ "nsphere p" f, unfolded o_def])
+        using f apply (simp add: nsphere)
+        by (simp add: continuous_map_nsphere_projection)
+      then have "continuous_map (prod_topology ?T01 (nsphere p)) euclideanreal (\<lambda>r. ?h r k)"
+        for k
+        unfolding case_prod_unfold o_def
+        by (intro continuous_map_into_fulltopology [OF continuous_map_fst] continuous_intros) auto
+      moreover have "?h ` ({0..1} \<times> topspace (nsphere p)) \<subseteq> {x. \<forall>i\<ge>Suc p. x i = 0}"
+        using continuous_map_image_subset_topspace [OF f]
+        by (auto simp: nsphere image_subset_iff a0)
+      moreover have "(\<lambda>i. 0) \<notin> ?h ` ({0..1} \<times> topspace (nsphere p))"
+      proof clarify
+        fix t b
+        assume eq: "(\<lambda>i. 0) = (\<lambda>i. (1 - t) * f b i - t * a i)" and "t \<in> {0..1}" and b: "b \<in> topspace (nsphere p)"
+        have "(1 - t)\<^sup>2 = (\<Sum>i\<le>p. ((1 - t) * f b i)^2)"
+          using f1 [OF b] by (simp add: power_mult_distrib flip: sum_distrib_left)
+        also have "\<dots> = (\<Sum>i\<le>p. (t * a i)^2)"
+          using eq by (simp add: fun_eq_iff)
+        also have "\<dots> = t\<^sup>2"
+          using a1 by (simp add: power_mult_distrib flip: sum_distrib_left)
+        finally have "1 - t = t"
+          by (simp add: power2_eq_iff)
+        then have *: "t = 1/2"
+          by simp
+        have fba: "f b \<noteq> a"
+          using a(2) b by blast
+        then show False
+          using eq unfolding * by (simp add: fun_eq_iff)
+      qed
+      ultimately show "continuous_map (prod_topology ?T01 (nsphere p)) ?Y ?h"
+        by (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV)
+    next
+      have *: "\<lbrakk>\<forall>i\<ge>Suc p. x i = 0; x \<noteq> (\<lambda>i. 0)\<rbrakk> \<Longrightarrow> (\<Sum>j\<le>p. (x j)\<^sup>2) \<noteq> 0" for x :: "nat \<Rightarrow> real"
+        by (force simp: fun_eq_iff not_less_eq_eq sum_nonneg_eq_0_iff)
+      show "continuous_map ?Y (nsphere p) ?g"
+        apply (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
+                         nsphere continuous_map_componentwise subtopology_subtopology)
+        apply (intro conjI allI continuous_intros continuous_map_from_subtopology [OF continuous_map_product_projection])
+            apply (simp_all add: *)
+         apply (force simp: sum_nonneg fun_eq_iff not_less_eq_eq sum_nonneg_eq_0_iff power_divide simp flip: sum_divide_distrib)
+        done
+    qed
+    have 2: "(?g \<circ> ?h) (0, x) = f x" if "x \<in> topspace (nsphere p)" for x
+      using that f1 by simp
+    have 3: "(?g \<circ> ?h) (1, x) = (\<lambda>i. - a i)" for x
+      using a by (force simp: divide_simps nsphere)
+    then show "homotopic_with (\<lambda>x. True) (nsphere p) (nsphere p) f (\<lambda>x. (\<lambda>i. - a i))"
+      by (force simp: homotopic_with intro: 1 2 3)
+  qed
+qed
+
+lemma Hausdorff_Euclidean_space:
+   "Hausdorff_space (Euclidean_space n)"
+  unfolding Euclidean_space_def
+  by (rule Hausdorff_space_subtopology) (metis Hausdorff_space_euclidean euclidean_product_topology)
+
+end
+
diff -r 3fd083253a1c -r cf7150ab1075 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Wed Mar 27 14:08:26 2019 +0000
@@ -161,6 +161,12 @@
   apply (metis openin_subset subset_eq)
   done
 
+lemma topology_finer_closedin:
+  "topspace X = topspace Y \<Longrightarrow> (\<forall>S. openin Y S \<longrightarrow> openin X S) \<longleftrightarrow> (\<forall>S. closedin Y S \<longrightarrow> closedin X S)"
+  apply safe
+   apply (simp add: closedin_def)
+  by (simp add: openin_closedin_eq)
+
 lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
   by (simp add: openin_closedin_eq)
 
@@ -1611,7 +1617,7 @@
 
 declare continuous_map_const [THEN iffD2, continuous_intros]
 
-lemma continuous_map_compose:
+lemma continuous_map_compose [continuous_intros]:
   assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
   shows "continuous_map X X'' (g \<circ> f)"
   unfolding continuous_map_def
@@ -1711,10 +1717,10 @@
    "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sqrt(f x))"
   by (meson continuous_map_compose continuous_map_eq continuous_map_square_root o_apply)
 
-lemma continuous_map_id [simp]: "continuous_map X X id"
+lemma continuous_map_id [simp, continuous_intros]: "continuous_map X X id"
   unfolding continuous_map_def  using openin_subopen topspace_def by fastforce
 
-declare continuous_map_id [unfolded id_def, simp]
+declare continuous_map_id [unfolded id_def, simp, continuous_intros]
 
 lemma continuous_map_id_subt [simp]: "continuous_map (subtopology X S) X id"
   by (simp add: continuous_map_from_subtopology)
diff -r 3fd083253a1c -r cf7150ab1075 src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Analysis/Analysis.thy	Wed Mar 27 14:08:26 2019 +0000
@@ -6,7 +6,7 @@
   (* Topology *)
   Connected
   Abstract_Limits
-  Locally
+  Abstract_Euclidean_Space
   (* Functional Analysis *)
   Elementary_Normed_Spaces
   Norm_Arith
diff -r 3fd083253a1c -r cf7150ab1075 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Wed Mar 27 14:08:26 2019 +0000
@@ -78,6 +78,9 @@
   where "product_topology T I =
     topology_generated_by {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
 
+abbreviation powertop_real :: "'a set \<Rightarrow> ('a \<Rightarrow> real) topology"
+  where "powertop_real \<equiv> product_topology (\<lambda>i. euclideanreal)"
+
 text \<open>The total set of the product topology is the product of the total sets
 along each coordinate.\<close>
 
@@ -1994,5 +1997,55 @@
     PiE I S = {} \<or> (\<forall>i \<in> I. path_connectedin (X i) (S i))"
   by (fastforce simp add: path_connectedin_def subtopology_PiE path_connected_space_product_topology subset_PiE PiE_eq_empty_iff topspace_subtopology_subset)
 
+subsection \<open>Projections from a function topology to a component\<close>
+
+lemma quotient_map_product_projection:
+  assumes "i \<in> I"
+  shows "quotient_map(product_topology X I) (X i) (\<lambda>x. x i) \<longleftrightarrow>
+           (topspace(product_topology X I) = {} \<longrightarrow> topspace(X i) = {})"
+         (is "?lhs = ?rhs")
+proof
+  assume ?lhs with assms show ?rhs
+    by (auto simp: continuous_open_quotient_map open_map_product_projection)
+next
+  assume ?rhs with assms show ?lhs
+    by (auto simp: Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection)
+qed
+
+lemma product_topology_homeomorphic_component:
+  assumes "i \<in> I" "\<And>j. \<lbrakk>j \<in> I; j \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>a. topspace(X j) = {a}"
+  shows "product_topology X I homeomorphic_space (X i)"
+proof -
+  have "quotient_map (product_topology X I) (X i) (\<lambda>x. x i)"
+    using assms by (force simp add: quotient_map_product_projection PiE_eq_empty_iff)
+  moreover
+  have "inj_on (\<lambda>x. x i) (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+    using assms by (auto simp: inj_on_def PiE_iff) (metis extensionalityI singletonD)
+  ultimately show ?thesis
+    unfolding homeomorphic_space_def
+    by (rule_tac x="\<lambda>x. x i" in exI) (simp add: homeomorphic_map_def flip: homeomorphic_map_maps)
+qed
+
+lemma topological_property_of_product_component:
+  assumes major: "P (product_topology X I)"
+    and minor: "\<And>z i. \<lbrakk>z \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i)); P(product_topology X I); i \<in> I\<rbrakk> 
+                      \<Longrightarrow> P(subtopology (product_topology X I) (PiE I (\<lambda>j. if j = i then topspace(X i) else {z j})))"
+               (is "\<And>z i. \<lbrakk>_; _; _\<rbrakk> \<Longrightarrow> P (?SX z i)")
+    and PQ:  "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
+  shows "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {} \<or> (\<forall>i \<in> I. Q(X i))"
+proof -
+  have "Q(X i)" if "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) \<noteq> {}" "i \<in> I" for i
+  proof -
+    from that obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" 
+      by force
+    have "?SX f i homeomorphic_space X i"
+      apply (simp add: subtopology_PiE )
+      using product_topology_homeomorphic_component [OF \<open>i \<in> I\<close>, of "\<lambda>j. subtopology (X j) (if j = i then topspace (X i) else {f j})"]
+      using f by fastforce
+    then show ?thesis
+      using minor [OF f major \<open>i \<in> I\<close>] PQ by auto
+  qed
+  then show ?thesis by metis
+qed
 
 end
diff -r 3fd083253a1c -r cf7150ab1075 src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Analysis/Product_Topology.thy	Wed Mar 27 14:08:26 2019 +0000
@@ -214,6 +214,14 @@
 lemma continuous_map_snd_of [continuous_intros]:
    "continuous_map Z (prod_topology X Y) f \<Longrightarrow> continuous_map Z Y (snd \<circ> f)"
   by (simp add: continuous_map_pairwise)
+    
+lemma continuous_map_prod_fst: 
+  "i \<in> I \<Longrightarrow> continuous_map (prod_topology (product_topology (\<lambda>i. Y) I) X) Y (\<lambda>x. fst x i)"
+  using continuous_map_componentwise_UNIV continuous_map_fst by fastforce
+
+lemma continuous_map_prod_snd: 
+  "i \<in> I \<Longrightarrow> continuous_map (prod_topology X (product_topology (\<lambda>i. Y) I)) Y (\<lambda>x. snd x i)"
+  using continuous_map_componentwise_UNIV continuous_map_snd by fastforce
 
 lemma continuous_map_if_iff [simp]: "continuous_map X Y (\<lambda>x. if P then f x else g x) \<longleftrightarrow> continuous_map X Y (if P then f else g)"
   by simp
diff -r 3fd083253a1c -r cf7150ab1075 src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy	Wed Mar 27 14:08:26 2019 +0000
@@ -1,9 +1,11 @@
-section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
+section\<open>T1 and Hausdorff spaces\<close>
 
 theory T1_Spaces
 imports Product_Topology 
 begin
 
+section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
+
 definition t1_space where
  "t1_space X \<equiv> \<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x\<noteq>y \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> y \<notin> U)"
 
@@ -214,4 +216,442 @@
     by simp
 qed
 
+subsection\<open>Hausdorff Spaces\<close>
+
+definition Hausdorff_space
+  where
+ "Hausdorff_space X \<equiv>
+        \<forall>x y. x \<in> topspace X \<and> y \<in> topspace X \<and> (x \<noteq> y)
+              \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V)"
+
+lemma Hausdorff_space_expansive:
+   "\<lbrakk>Hausdorff_space X; topspace X = topspace Y; \<And>U. openin X U \<Longrightarrow> openin Y U\<rbrakk> \<Longrightarrow> Hausdorff_space Y"
+  by (metis Hausdorff_space_def)
+
+lemma Hausdorff_space_topspace_empty:
+   "topspace X = {} \<Longrightarrow> Hausdorff_space X"
+  by (simp add: Hausdorff_space_def)
+
+lemma Hausdorff_imp_t1_space:
+   "Hausdorff_space X \<Longrightarrow> t1_space X"
+  by (metis Hausdorff_space_def disjnt_iff t1_space_def)
+
+lemma closedin_derived_set_of:
+   "Hausdorff_space X \<Longrightarrow> closedin X (X derived_set_of S)"
+  by (simp add: Hausdorff_imp_t1_space closedin_derived_set_of_gen)
+
+lemma t1_or_Hausdorff_space:
+   "t1_space X \<or> Hausdorff_space X \<longleftrightarrow> t1_space X"
+  using Hausdorff_imp_t1_space by blast
+
+lemma Hausdorff_space_sing_Inter_opens:
+   "\<lbrakk>Hausdorff_space X; a \<in> topspace X\<rbrakk> \<Longrightarrow> \<Inter>{u. openin X u \<and> a \<in> u} = {a}"
+  using Hausdorff_imp_t1_space t1_space_singleton_Inter_open by force
+
+lemma Hausdorff_space_subtopology:
+  assumes "Hausdorff_space X" shows "Hausdorff_space(subtopology X S)"
+proof -
+  have *: "disjnt U V \<Longrightarrow> disjnt (S \<inter> U) (S \<inter> V)" for U V
+    by (simp add: disjnt_iff)
+  from assms show ?thesis
+    apply (simp add: Hausdorff_space_def openin_subtopology_alt)
+    apply (fast intro: * elim!: all_forward)
+    done
+qed
+
+lemma Hausdorff_space_compact_separation:
+  assumes X: "Hausdorff_space X" and S: "compactin X S" and T: "compactin X T" and "disjnt S T"
+  obtains U V where "openin X U" "openin X V" "S \<subseteq> U" "T \<subseteq> V" "disjnt U V"
+proof (cases "S = {}")
+  case True
+  then show thesis
+    by (metis \<open>compactin X T\<close> compactin_subset_topspace disjnt_empty1 empty_subsetI openin_empty openin_topspace that)
+next
+  case False
+  have "\<forall>x \<in> S. \<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> T \<subseteq> V \<and> disjnt U V"
+  proof
+    fix a
+    assume "a \<in> S"
+    then have "a \<notin> T"
+      by (meson assms(4) disjnt_iff)
+    have a: "a \<in> topspace X"
+      using S \<open>a \<in> S\<close> compactin_subset_topspace by blast
+    show "\<exists>U V. openin X U \<and> openin X V \<and> a \<in> U \<and> T \<subseteq> V \<and> disjnt U V"
+    proof (cases "T = {}")
+      case True
+      then show ?thesis
+        using a disjnt_empty2 openin_empty by blast
+    next
+      case False
+      have "\<forall>x \<in> topspace X - {a}. \<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> a \<in> V \<and> disjnt U V"
+        using X a by (simp add: Hausdorff_space_def)
+      then obtain U V where UV: "\<forall>x \<in> topspace X - {a}. openin X (U x) \<and> openin X (V x) \<and> x \<in> U x \<and> a \<in> V x \<and> disjnt (U x) (V x)"
+        by metis
+      with \<open>a \<notin> T\<close> compactin_subset_topspace [OF T]
+      have Topen: "\<forall>W \<in> U ` T. openin X W" and Tsub: "T \<subseteq> \<Union> (U ` T)"
+        by (auto simp: )
+      then obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> U ` T" and "T \<subseteq> \<Union>\<F>"
+        using T unfolding compactin_def by meson
+      then obtain F where F: "finite F" "F \<subseteq> T" "\<F> = U ` F" and SUF: "T \<subseteq> \<Union>(U ` F)" and "a \<notin> F"
+        using finite_subset_image [OF \<F>] \<open>a \<notin> T\<close> by (metis subsetD)
+      have U: "\<And>x. \<lbrakk>x \<in> topspace X; x \<noteq> a\<rbrakk> \<Longrightarrow> openin X (U x)"
+        and V: "\<And>x. \<lbrakk>x \<in> topspace X; x \<noteq> a\<rbrakk> \<Longrightarrow> openin X (V x)"
+        and disj: "\<And>x. \<lbrakk>x \<in> topspace X; x \<noteq> a\<rbrakk> \<Longrightarrow> disjnt (U x) (V x)"
+        using UV by blast+
+      show ?thesis
+      proof (intro exI conjI)
+        have "F \<noteq> {}"
+          using False SUF by blast
+        with \<open>a \<notin> F\<close> show "openin X (\<Inter>(V ` F))"
+          using F compactin_subset_topspace [OF T] by (force intro: V)
+        show "openin X (\<Union>(U ` F))"
+          using F Topen Tsub by (force intro: U)
+        show "disjnt (\<Inter>(V ` F)) (\<Union>(U ` F))"
+          using disj
+          apply (auto simp: disjnt_def)
+          using \<open>F \<subseteq> T\<close> \<open>a \<notin> F\<close> compactin_subset_topspace [OF T] by blast
+        show "a \<in> (\<Inter>(V ` F))"
+          using \<open>F \<subseteq> T\<close> T UV \<open>a \<notin> T\<close> compactin_subset_topspace by blast
+      qed (auto simp: SUF)
+    qed
+  qed
+  then obtain U V where UV: "\<forall>x \<in> S. openin X (U x) \<and> openin X (V x) \<and> x \<in> U x \<and> T \<subseteq> V x \<and> disjnt (U x) (V x)"
+    by metis
+  then have "S \<subseteq> \<Union> (U ` S)"
+    by auto
+  moreover have "\<forall>W \<in> U ` S. openin X W"
+    using UV by blast
+  ultimately obtain I where I: "S \<subseteq> \<Union> (U ` I)" "I \<subseteq> S" "finite I"
+    by (metis S compactin_def finite_subset_image)
+  show thesis
+  proof
+    show "openin X (\<Union>(U ` I))"
+      using \<open>I \<subseteq> S\<close> UV by blast
+    show "openin X (\<Inter> (V ` I))"
+      using False UV \<open>I \<subseteq> S\<close> \<open>S \<subseteq> \<Union> (U ` I)\<close> \<open>finite I\<close> by blast
+    show "disjnt (\<Union>(U ` I)) (\<Inter> (V ` I))"
+      by simp (meson UV \<open>I \<subseteq> S\<close> disjnt_subset2 in_mono le_INF_iff order_refl)
+  qed (use UV I in auto)
+qed
+
+
+lemma Hausdorff_space_compact_sets:
+  "Hausdorff_space X \<longleftrightarrow>
+    (\<forall>S T. compactin X S \<and> compactin X T \<and> disjnt S T
+           \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V))"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (meson Hausdorff_space_compact_separation)
+next
+  assume R [rule_format]: ?rhs
+  show ?lhs
+  proof (clarsimp simp add: Hausdorff_space_def)
+    fix x y
+    assume "x \<in> topspace X" "y \<in> topspace X" "x \<noteq> y"
+    then show "\<exists>U. openin X U \<and> (\<exists>V. openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V)"
+      using R [of "{x}" "{y}"] by auto
+  qed
+qed
+
+lemma compactin_imp_closedin:
+  assumes X: "Hausdorff_space X" and S: "compactin X S" shows "closedin X S"
+proof -
+  have "S \<subseteq> topspace X"
+    by (simp add: assms compactin_subset_topspace)
+  moreover
+  have "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> topspace X - S" if "x \<in> topspace X" "x \<notin> S" for x
+    using Hausdorff_space_compact_separation [OF X _ S, of "{x}"] that
+    apply (simp add: disjnt_def)
+    by (metis Diff_mono Diff_triv openin_subset)
+  ultimately show ?thesis
+    using closedin_def openin_subopen by force
+qed
+
+lemma closedin_Hausdorff_singleton:
+   "\<lbrakk>Hausdorff_space X; x \<in> topspace X\<rbrakk> \<Longrightarrow> closedin X {x}"
+  by (simp add: Hausdorff_imp_t1_space closedin_t1_singleton)
+
+lemma closedin_Hausdorff_sing_eq:
+   "Hausdorff_space X \<Longrightarrow> closedin X {x} \<longleftrightarrow> x \<in> topspace X"
+  by (meson closedin_Hausdorff_singleton closedin_subset insert_subset)
+
+lemma Hausdorff_space_discrete_topology [simp]:
+   "Hausdorff_space (discrete_topology U)"
+  unfolding Hausdorff_space_def
+  apply safe
+  by (metis discrete_topology_unique_alt disjnt_empty2 disjnt_insert2 insert_iff mk_disjoint_insert topspace_discrete_topology)
+
+lemma compactin_Int:
+   "\<lbrakk>Hausdorff_space X; compactin X S; compactin X T\<rbrakk> \<Longrightarrow> compactin X (S \<inter> T)"
+  by (simp add: closed_Int_compactin compactin_imp_closedin)
+
+lemma finite_topspace_imp_discrete_topology:
+   "\<lbrakk>topspace X = U; finite U; Hausdorff_space X\<rbrakk> \<Longrightarrow> X = discrete_topology U"
+  using Hausdorff_imp_t1_space finite_t1_space_imp_discrete_topology by blast
+
+lemma derived_set_of_finite:
+   "\<lbrakk>Hausdorff_space X; finite S\<rbrakk> \<Longrightarrow> X derived_set_of S = {}"
+  using Hausdorff_imp_t1_space t1_space_derived_set_of_finite by auto
+
+lemma derived_set_of_singleton:
+   "Hausdorff_space X \<Longrightarrow> X derived_set_of {x} = {}"
+  by (simp add: derived_set_of_finite)
+
+lemma closedin_Hausdorff_finite:
+   "\<lbrakk>Hausdorff_space X; S \<subseteq> topspace X; finite S\<rbrakk> \<Longrightarrow> closedin X S"
+  by (simp add: compactin_imp_closedin finite_imp_compactin_eq)
+
+lemma open_in_Hausdorff_delete:
+   "\<lbrakk>Hausdorff_space X; openin X S\<rbrakk> \<Longrightarrow> openin X (S - {x})"
+  using Hausdorff_imp_t1_space t1_space_openin_delete_alt by auto
+
+lemma closedin_Hausdorff_finite_eq:
+   "\<lbrakk>Hausdorff_space X; finite S\<rbrakk> \<Longrightarrow> closedin X S \<longleftrightarrow> S \<subseteq> topspace X"
+  by (meson closedin_Hausdorff_finite closedin_def)
+
+lemma derived_set_of_infinite_open_in:
+   "Hausdorff_space X
+        \<Longrightarrow> X derived_set_of S =
+            {x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)}"
+  using Hausdorff_imp_t1_space t1_space_derived_set_of_infinite_openin by fastforce
+
+lemma Hausdorff_space_discrete_compactin:
+   "Hausdorff_space X
+        \<Longrightarrow> S \<inter> X derived_set_of S = {} \<and> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
+  using derived_set_of_finite discrete_compactin_eq_finite by fastforce
+
+lemma Hausdorff_space_finite_topspace:
+   "Hausdorff_space X \<Longrightarrow> X derived_set_of (topspace X) = {} \<and> compact_space X \<longleftrightarrow> finite(topspace X)"
+  using derived_set_of_finite discrete_compact_space_eq_finite by auto
+
+lemma derived_set_of_derived_set_subset:
+   "Hausdorff_space X \<Longrightarrow> X derived_set_of (X derived_set_of S) \<subseteq> X derived_set_of S"
+  by (simp add: Hausdorff_imp_t1_space derived_set_of_derived_set_subset_gen)
+
+
+lemma Hausdorff_space_injective_preimage:
+  assumes "Hausdorff_space Y" and cmf: "continuous_map X Y f" and "inj_on f (topspace X)"
+  shows "Hausdorff_space X"
+  unfolding Hausdorff_space_def
+proof clarify
+  fix x y
+  assume x: "x \<in> topspace X" and y: "y \<in> topspace X" and "x \<noteq> y"
+  then obtain U V where "openin Y U" "openin Y V" "f x \<in> U" "f y \<in> V" "disjnt U V"
+    using assms unfolding Hausdorff_space_def continuous_map_def by (meson inj_onD)
+  show "\<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
+  proof (intro exI conjI)
+    show "openin X {x \<in> topspace X. f x \<in> U}"
+      using \<open>openin Y U\<close> cmf continuous_map by fastforce
+    show "openin X {x \<in> topspace X. f x \<in> V}"
+      using \<open>openin Y V\<close> cmf openin_continuous_map_preimage by blast
+    show "disjnt {x \<in> topspace X. f x \<in> U} {x \<in> topspace X. f x \<in> V}"
+      using \<open>disjnt U V\<close> by (auto simp add: disjnt_def)
+  qed (use x \<open>f x \<in> U\<close> y \<open>f y \<in> V\<close> in auto)
+qed
+
+lemma homeomorphic_Hausdorff_space:
+   "X homeomorphic_space Y \<Longrightarrow> Hausdorff_space X \<longleftrightarrow> Hausdorff_space Y"
+  unfolding homeomorphic_space_def homeomorphic_maps_map
+  by (auto simp: homeomorphic_eq_everything_map Hausdorff_space_injective_preimage)
+
+lemma Hausdorff_space_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; Hausdorff_space X\<rbrakk> \<Longrightarrow> Hausdorff_space Y"
+  unfolding retraction_map_def
+  using Hausdorff_space_subtopology homeomorphic_Hausdorff_space retraction_maps_section_image2 by blast
+
+lemma compact_Hausdorff_space_optimal:
+  assumes eq: "topspace Y = topspace X" and XY: "\<And>U. openin X U \<Longrightarrow> openin Y U"
+      and "Hausdorff_space X" "compact_space Y"
+    shows "Y = X"
+proof -
+  have "\<And>U. closedin X U \<Longrightarrow> closedin Y U"
+    using XY using topology_finer_closedin [OF eq]
+    by metis
+  have "openin Y S = openin X S" for S
+    by (metis XY assms(3) assms(4) closedin_compact_space compactin_contractive compactin_imp_closedin eq openin_closedin_eq)
+  then show ?thesis
+    by (simp add: topology_eq)
+qed
+
+lemma continuous_imp_closed_map:
+   "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f\<rbrakk> \<Longrightarrow> closed_map X Y f"
+  by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin)
+
+lemma continuous_imp_quotient_map:
+   "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f; f ` (topspace X) = topspace Y\<rbrakk>
+        \<Longrightarrow> quotient_map X Y f"
+  by (simp add: continuous_imp_closed_map continuous_closed_imp_quotient_map)
+
+lemma continuous_imp_homeomorphic_map:
+   "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f;
+     f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
+        \<Longrightarrow> homeomorphic_map X Y f"
+  by (simp add: continuous_imp_closed_map bijective_closed_imp_homeomorphic_map)
+
+lemma continuous_imp_embedding_map:
+   "\<lbrakk>compact_space X; Hausdorff_space Y; continuous_map X Y f; inj_on f (topspace X)\<rbrakk>
+        \<Longrightarrow> embedding_map X Y f"
+  by (simp add: continuous_imp_closed_map injective_closed_imp_embedding_map)
+
+lemma continuous_inverse_map:
+  assumes "compact_space X" "Hausdorff_space Y"
+    and cmf: "continuous_map X Y f" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
+    and Sf:  "S \<subseteq> f ` (topspace X)"
+  shows "continuous_map (subtopology Y S) X g"
+proof (rule continuous_map_from_subtopology_mono [OF _ \<open>S \<subseteq> f ` (topspace X)\<close>])
+  show "continuous_map (subtopology Y (f ` (topspace X))) X g"
+    unfolding continuous_map_closedin
+  proof (intro conjI ballI allI impI)
+    fix x
+    assume "x \<in> topspace (subtopology Y (f ` topspace X))"
+    then show "g x \<in> topspace X"
+      by (auto simp: gf)
+  next
+    fix C
+    assume C: "closedin X C"
+    show "closedin (subtopology Y (f ` topspace X))
+           {x \<in> topspace (subtopology Y (f ` topspace X)). g x \<in> C}"
+    proof (rule compactin_imp_closedin)
+      show "Hausdorff_space (subtopology Y (f ` topspace X))"
+        using Hausdorff_space_subtopology [OF \<open>Hausdorff_space Y\<close>] by blast
+      have "compactin Y (f ` C)"
+        using C cmf image_compactin closedin_compact_space [OF \<open>compact_space X\<close>] by blast
+      moreover have "{x \<in> topspace Y. x \<in> f ` topspace X \<and> g x \<in> C} = f ` C"
+        using closedin_subset [OF C] cmf by (auto simp: gf continuous_map_def)
+      ultimately have "compactin Y {x \<in> topspace Y. x \<in> f ` topspace X \<and> g x \<in> C}"
+        by simp
+      then show "compactin (subtopology Y (f ` topspace X))
+              {x \<in> topspace (subtopology Y (f ` topspace X)). g x \<in> C}"
+        by (auto simp add: compactin_subtopology)
+    qed
+  qed
+qed
+
+
+lemma Hausdorff_space_euclidean: "Hausdorff_space (euclidean :: 'a::metric_space topology)"
+proof -
+  have "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
+    if "x \<noteq> y"
+    for x y :: 'a
+  proof (intro exI conjI)
+    let ?r = "dist x y / 2"
+    have [simp]: "?r > 0"
+      by (simp add: that)
+    show "open (ball x ?r)" "open (ball y ?r)" "x \<in> (ball x ?r)" "y \<in> (ball y ?r)"
+      by (auto simp add: that)
+    show "disjnt (ball x ?r) (ball y ?r)"
+      unfolding disjnt_def by (simp add: disjoint_ballI)
+  qed
+  then show ?thesis
+    by (simp add: Hausdorff_space_def)
+qed
+
+lemma Hausdorff_space_prod_topology:
+  "Hausdorff_space(prod_topology X Y) \<longleftrightarrow> topspace(prod_topology X Y) = {} \<or> Hausdorff_space X \<and> Hausdorff_space Y"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (rule topological_property_of_prod_component) (auto simp: Hausdorff_space_subtopology homeomorphic_Hausdorff_space)
+next
+  assume R: ?rhs
+  show ?lhs
+  proof (cases "(topspace X \<times> topspace Y) = {}")
+    case False
+    with R have ne: "topspace X \<noteq> {}" "topspace Y \<noteq> {}" and X: "Hausdorff_space X" and Y: "Hausdorff_space Y"
+      by auto
+    show ?thesis
+      unfolding Hausdorff_space_def
+    proof clarify
+      fix x y x' y'
+      assume xy: "(x, y) \<in> topspace (prod_topology X Y)"
+        and xy': "(x',y') \<in> topspace (prod_topology X Y)"
+        and *: "\<nexists>U V. openin (prod_topology X Y) U \<and> openin (prod_topology X Y) V
+               \<and> (x, y) \<in> U \<and> (x', y') \<in> V \<and> disjnt U V"
+      have False if "x \<noteq> x' \<or> y \<noteq> y'"
+        using that
+      proof
+        assume "x \<noteq> x'"
+        then obtain U V where "openin X U" "openin X V" "x \<in> U" "x' \<in> V" "disjnt U V"
+          by (metis Hausdorff_space_def X mem_Sigma_iff topspace_prod_topology xy xy')
+        let ?U = "U \<times> topspace Y"
+        let ?V = "V \<times> topspace Y"
+        have "openin (prod_topology X Y) ?U" "openin (prod_topology X Y) ?V"
+          by (simp_all add: openin_prod_Times_iff \<open>openin X U\<close> \<open>openin X V\<close>)
+        moreover have "disjnt ?U ?V"
+          by (simp add: \<open>disjnt U V\<close>)
+        ultimately show False
+          using * \<open>x \<in> U\<close> \<open>x' \<in> V\<close> xy xy' by (metis SigmaD2 SigmaI topspace_prod_topology)
+      next
+        assume "y \<noteq> y'"
+        then obtain U V where "openin Y U" "openin Y V" "y \<in> U" "y' \<in> V" "disjnt U V"
+          by (metis Hausdorff_space_def Y mem_Sigma_iff topspace_prod_topology xy xy')
+        let ?U = "topspace X \<times> U"
+        let ?V = "topspace X \<times> V"
+        have "openin (prod_topology X Y) ?U" "openin (prod_topology X Y) ?V"
+          by (simp_all add: openin_prod_Times_iff \<open>openin Y U\<close> \<open>openin Y V\<close>)
+        moreover have "disjnt ?U ?V"
+          by (simp add: \<open>disjnt U V\<close>)
+        ultimately show False
+          using "*" \<open>y \<in> U\<close> \<open>y' \<in> V\<close> xy xy' by (metis SigmaD1 SigmaI topspace_prod_topology)
+      qed
+      then show "x = x' \<and> y = y'"
+        by blast
+    qed
+  qed (simp add: Hausdorff_space_topspace_empty)
+qed
+
+
+lemma Hausdorff_space_product_topology:
+   "Hausdorff_space (product_topology X I) \<longleftrightarrow> (\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {} \<or> (\<forall>i \<in> I. Hausdorff_space (X i))"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    apply (rule topological_property_of_product_component)
+     apply (blast dest: Hausdorff_space_subtopology homeomorphic_Hausdorff_space)+
+    done
+next
+  assume R: ?rhs
+  show ?lhs
+  proof (cases "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {}")
+    case True
+    then show ?thesis
+      by (simp add: Hausdorff_space_topspace_empty)
+  next
+    case False
+    have "\<exists>U V. openin (product_topology X I) U \<and> openin (product_topology X I) V \<and> f \<in> U \<and> g \<in> V \<and> disjnt U V"
+      if f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" and g: "g \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" and "f \<noteq> g"
+      for f g :: "'a \<Rightarrow> 'b"
+    proof -
+      obtain m where "f m \<noteq> g m"
+        using \<open>f \<noteq> g\<close> by blast
+      then have "m \<in> I"
+        using f g by fastforce
+      then have "Hausdorff_space (X m)" 
+        using False that R by blast
+      then obtain U V where U: "openin (X m) U" and V: "openin (X m) V" and "f m \<in> U" "g m \<in> V" "disjnt U V"
+        by (metis Hausdorff_space_def PiE_mem \<open>f m \<noteq> g m\<close> \<open>m \<in> I\<close> f g)
+      show ?thesis
+      proof (intro exI conjI)
+        let ?U = "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) \<inter> {x. x m \<in> U}"
+        let ?V = "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) \<inter> {x. x m \<in> V}"
+        show "openin (product_topology X I) ?U" "openin (product_topology X I) ?V"
+          using \<open>m \<in> I\<close> U V
+          by (force simp add: openin_product_topology intro: arbitrary_union_of_inc relative_to_inc finite_intersection_of_inc)+
+        show "f \<in> ?U"
+          using \<open>f m \<in> U\<close> f by blast
+        show "g \<in> ?V"
+          using \<open>g m \<in> V\<close> g by blast
+        show "disjnt ?U ?V"
+          using \<open>disjnt U V\<close> by (auto simp: PiE_def Pi_def disjnt_def)
+        qed
+    qed
+    then show ?thesis
+      by (simp add: Hausdorff_space_def)   
+  qed
+qed
+
 end
diff -r 3fd083253a1c -r cf7150ab1075 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Product_Type.thy	Wed Mar 27 14:08:26 2019 +0000
@@ -1272,6 +1272,17 @@
        proc = K Set_Comprehension_Pointfree.code_simproc}])
 \<close>
 
+subsection \<open>Lemmas about disjointness\<close>
+
+lemma disjnt_Times1_iff [simp]: "disjnt (C \<times> A) (C \<times> B) \<longleftrightarrow> C = {} \<or> disjnt A B"
+  by (auto simp: disjnt_def)
+
+lemma disjnt_Times2_iff [simp]: "disjnt (A \<times> C) (B \<times> C) \<longleftrightarrow> C = {} \<or> disjnt A B"
+  by (auto simp: disjnt_def)
+
+lemma disjnt_Sigma_iff: "disjnt (Sigma A C) (Sigma B C) \<longleftrightarrow> (\<forall>i \<in> A\<inter>B. C i = {}) \<or> disjnt A B"
+  by (auto simp: disjnt_def)
+
 
 subsection \<open>Inductively defined sets\<close>