# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1553177902 0
# Node ID 812ce526da3396f9a6eff341bf2bf6a7780deccd
# Parent  c15ee153dec18ee14693e60d971276d57386fc93
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map

diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -1410,7 +1410,10 @@
   by (simp add: Sup_le_iff closure_of_minimal)
 
 
-subsection\<open>Continuous maps\<close>
+subsection%important \<open>Continuous maps\<close>
+
+text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
+of type classes, as defined below.\<close>
 
 definition continuous_map where
   "continuous_map X Y f \<equiv>
@@ -1717,6 +1720,22 @@
 declare continuous_map_id_subt [unfolded id_def, simp]
 
 
+lemma%important continuous_map_alt:
+   "continuous_map T1 T2 f 
+    = ((\<forall>U. openin T2 U \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)) \<and> f ` topspace T1 \<subseteq> topspace T2)"
+  by (auto simp: continuous_map_def vimage_def image_def Collect_conj_eq inf_commute)
+
+lemma continuous_map_open [intro]:
+  "continuous_map T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
+  unfolding continuous_map_alt by auto
+
+lemma continuous_map_preimage_topspace [intro]:
+  assumes "continuous_map T1 T2 f"
+  shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
+using assms unfolding continuous_map_def by auto
+
+
+
 subsection\<open>Open and closed maps (not a priori assumed continuous)\<close>
 
 definition open_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
@@ -1852,7 +1871,7 @@
   apply clarify
   apply (rename_tac T)
   apply (rule_tac x="f ` T" in image_eqI)
-  using openin_closedin_eq by force+
+  using openin_closedin_eq by fastforce+
 
 lemma closed_map_restriction:
      "\<lbrakk>closed_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
@@ -1861,7 +1880,7 @@
   apply clarify
   apply (rename_tac T)
   apply (rule_tac x="f ` T" in image_eqI)
-  using closedin_def by force+
+  using closedin_def by fastforce+
 
 subsection\<open>Quotient maps\<close>
                                       
@@ -4177,35 +4196,10 @@
   qed
 qed
 
-subsubsection%important \<open>Continuity\<close>
-
-text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
-of type classes, as defined below.\<close>
-
-definition%important continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
-  where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
-                                      \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
-
-lemma continuous_on_continuous_on_topo:
-  "continuous_on s f \<longleftrightarrow> continuous_on_topo (top_of_set s) euclidean f"
-  by (auto simp: continuous_on_topo_def Int_commute continuous_openin_preimage_eq)
-
-lemma continuous_on_topo_UNIV:
-  "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
-using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto
-
-lemma continuous_on_topo_open [intro]:
-  "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
-  unfolding continuous_on_topo_def by auto
-
-lemma continuous_on_topo_topspace [intro]:
-  "continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
-unfolding continuous_on_topo_def by auto
-
 lemma continuous_on_generated_topo_iff:
-  "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
+  "continuous_map T1 (topology_generated_by S) f \<longleftrightarrow>
       ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
-unfolding continuous_on_topo_def topology_generated_by_topspace
+unfolding continuous_map_alt topology_generated_by_topspace
 proof (auto simp add: topology_generated_by_Basis)
   assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
   fix U assume "openin (topology_generated_by S) U"
@@ -4231,31 +4225,11 @@
 lemma continuous_on_generated_topo:
   assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
           "f`(topspace T1) \<subseteq> (\<Union> S)"
-  shows "continuous_on_topo T1 (topology_generated_by S) f"
+  shows "continuous_map T1 (topology_generated_by S) f"
   using assms continuous_on_generated_topo_iff by blast
 
-proposition continuous_on_topo_compose:
-  assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
-  shows "continuous_on_topo T1 T3 (g o f)"
-  using assms unfolding continuous_on_topo_def
-proof (auto)
-  fix U :: "'c set"
-  assume H: "openin T3 U"
-  have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
-    using H assms by blast
-  moreover have "f -` (g -` U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) -` U \<inter> topspace T1"
-    using H assms continuous_on_topo_topspace by fastforce
-  ultimately show "openin T1 ((g \<circ> f) -` U \<inter> topspace T1)"
-    by simp
-qed (blast)
-
-lemma continuous_on_topo_preimage_topspace [intro]:
-  assumes "continuous_on_topo T1 T2 f"
-  shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
-using assms unfolding continuous_on_topo_def by auto
-
-
-subsubsection%important \<open>Pullback topology\<close>
+
+subsection%important \<open>Pullback topology\<close>
 
 text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
 a special case of this notion, pulling back by the identity. We introduce the general notion as
@@ -4289,14 +4263,14 @@
   "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
 by (auto simp add: topspace_def openin_pullback_topology)
 
-proposition continuous_on_topo_pullback [intro]:
-  assumes "continuous_on_topo T1 T2 g"
-  shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
-unfolding continuous_on_topo_def
+proposition continuous_map_pullback [intro]:
+  assumes "continuous_map T1 T2 g"
+  shows "continuous_map (pullback_topology A f T1) T2 (g o f)"
+unfolding continuous_map_alt
 proof (auto)
   fix U::"'b set" assume "openin T2 U"
   then have "openin T1 (g-`U \<inter> topspace T1)"
-    using assms unfolding continuous_on_topo_def by auto
+    using assms unfolding continuous_map_alt by auto
   have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
     unfolding topspace_pullback_topology by auto
   also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
@@ -4310,13 +4284,13 @@
   then have "f x \<in> topspace T1"
     unfolding topspace_pullback_topology by auto
   then show "g (f x) \<in> topspace T2"
-    using assms unfolding continuous_on_topo_def by auto
+    using assms unfolding continuous_map_def by auto
 qed
 
-proposition continuous_on_topo_pullback' [intro]:
-  assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
-  shows "continuous_on_topo T1 (pullback_topology A f T2) g"
-unfolding continuous_on_topo_def
+proposition continuous_map_pullback' [intro]:
+  assumes "continuous_map T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
+  shows "continuous_map T1 (pullback_topology A f T2) g"
+unfolding continuous_map_alt
 proof (auto)
   fix U assume "openin (pullback_topology A f T2) U"
   then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
@@ -4335,7 +4309,7 @@
 next
   fix x assume "x \<in> topspace T1"
   have "(f o g) x \<in> topspace T2"
-    using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
+    using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
   then have "g x \<in> f-`(topspace T2)"
     unfolding comp_def by blast
   moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -1231,6 +1231,15 @@
 lemma pathin_const:
    "pathin X (\<lambda>x. a) \<longleftrightarrow> a \<in> topspace X"
   by (simp add: pathin_def)
+   
+lemma path_start_in_topspace: "pathin X g \<Longrightarrow> g 0 \<in> topspace X"
+  by (force simp: pathin_def continuous_map)
+
+lemma path_finish_in_topspace: "pathin X g \<Longrightarrow> g 1 \<in> topspace X"
+  by (force simp: pathin_def continuous_map)
+
+lemma path_image_subset_topspace: "pathin X g \<Longrightarrow> g ` ({0..1}) \<subseteq> topspace X"
+  by (force simp: pathin_def continuous_map)
 
 definition path_connected_space :: "'a topology \<Rightarrow> bool"
   where "path_connected_space X \<equiv> \<forall>x \<in> topspace X. \<forall> y \<in> topspace X. \<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y"
@@ -1323,6 +1332,19 @@
   qed
 qed
 
+lemma path_connectedin_discrete_topology:
+  "path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
+  apply safe
+  using path_connectedin_subset_topspace apply fastforce
+   apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
+  using subset_singletonD by fastforce
+
+lemma path_connected_space_discrete_topology:
+   "path_connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
+  by (metis path_connectedin_discrete_topology path_connectedin_topspace path_connected_space_topspace_empty
+            subset_singletonD topspace_discrete_topology)
+
+
 lemma homeomorphic_path_connected_space_imp:
      "\<lbrakk>path_connected_space X; X homeomorphic_space Y\<rbrakk> \<Longrightarrow> path_connected_space Y"
   unfolding homeomorphic_space_def homeomorphic_maps_def
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Analysis/Binary_Product_Measure.thy
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -74,11 +74,11 @@
 qed
 
 lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^sub>M M2) M1"
-  by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
+  by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space Times_Int_Times
     measurable_def)
 
 lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^sub>M M2) M2"
-  by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
+  by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space Times_Int_Times
     measurable_def)
 
 lemma measurable_Pair_compose_split[measurable_dest]:
@@ -215,7 +215,7 @@
 
 lemma Int_stable_pair_measure_generator: "Int_stable {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}"
   unfolding Int_stable_def
-  by safe (auto simp add: times_Int_times)
+  by safe (auto simp add: Times_Int_Times)
 
 lemma (in finite_measure) finite_measure_cut_measurable:
   assumes [measurable]: "Q \<in> sets (N \<Otimes>\<^sub>M M)"
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -779,41 +779,41 @@
 qed
 
 lemma strong_operator_topology_continuous_evaluation:
-  "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
+  "continuous_map strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
 proof -
-  have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
-    unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
-    using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
+  have "continuous_map strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
+    unfolding strong_operator_topology_def apply (rule continuous_map_pullback)
+    using continuous_on_product_coordinates by fastforce
   then show ?thesis unfolding comp_def by simp
 qed
 
 lemma continuous_on_strong_operator_topo_iff_coordinatewise:
-  "continuous_on_topo T strong_operator_topology f
-    \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
+  "continuous_map T strong_operator_topology f
+    \<longleftrightarrow> (\<forall>x. continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x))"
 proof (auto)
   fix x::"'b"
-  assume "continuous_on_topo T strong_operator_topology f"
-  with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
-  have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
+  assume "continuous_map T strong_operator_topology f"
+  with continuous_map_compose[OF this strong_operator_topology_continuous_evaluation]
+  have "continuous_map T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
     by simp
-  then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+  then show "continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x)"
     unfolding comp_def by auto
 next
-  assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
-  have "continuous_on_topo T euclidean (blinfun_apply o f)"
+  assume *: "\<forall>x. continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x)"
+  have "continuous_map T euclidean (blinfun_apply o f)"
     unfolding euclidean_product_topology
-    apply (rule continuous_on_topo_coordinatewise_then_product, auto)
+    apply (rule continuous_map_coordinatewise_then_product, auto)
     using * unfolding comp_def by auto
-  show "continuous_on_topo T strong_operator_topology f"
+  show "continuous_map T strong_operator_topology f"
     unfolding strong_operator_topology_def
-    apply (rule continuous_on_topo_pullback')
-    by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
+    apply (rule continuous_map_pullback')
+    by (auto simp add: \<open>continuous_map T euclidean (blinfun_apply o f)\<close>)
 qed
 
 lemma strong_operator_topology_weaker_than_euclidean:
-  "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
+  "continuous_map euclidean strong_operator_topology (\<lambda>f. f)"
   by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
-    auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
+    auto simp add: linear_continuous_on)
 
 
 
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -3,11 +3,11 @@
 *)
 
 theory Function_Topology
-imports Topology_Euclidean_Space   
+imports Topology_Euclidean_Space
 begin
 
 
-section \<open>Function Topology\<close> 
+section \<open>Function Topology\<close>
 
 text \<open>We want to define the general product topology.
 
@@ -42,17 +42,17 @@
 
 Here is an example of a reformulation using topologies. Let
 @{text [display]
-\<open>continuous_on_topo T1 T2 f =
+\<open>continuous_map T1 T2 f =
     ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
             \<and> (f`(topspace T1) \<subseteq> (topspace T2)))\<close>}
 be the natural continuity definition of a map from the topology \<open>T1\<close> to the topology \<open>T2\<close>. Then
 the current \<open>continuous_on\<close> (with type classes) can be redefined as
 @{text [display] \<open>continuous_on s f =
-    continuous_on_topo (top_of_set s) (topology euclidean) f\<close>}
+    continuous_map (top_of_set s) (topology euclidean) f\<close>}
 
-In fact, I need \<open>continuous_on_topo\<close> to express the continuity of the projection on subfactors
+In fact, I need \<open>continuous_map\<close> to express the continuity of the projection on subfactors
 for the product topology, in Lemma~\<open>continuous_on_restrict_product_topology\<close>, and I show
-the above equivalence in Lemma~\<open>continuous_on_continuous_on_topo\<close>.
+the above equivalence in Lemma~\<open>continuous_map_iff_continuous\<close>.
 
 I only develop the basics of the product topology in this theory. The most important missing piece
 is Tychonov theorem, stating that a product of compact spaces is always compact for the product
@@ -252,7 +252,7 @@
           ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
            relative_to topspace (product_topology X I))"
   apply (subst product_topology)
-  apply (simp add: topspace_product_topology topology_inverse' [OF istopology_subbase])
+  apply (simp add: topology_inverse' [OF istopology_subbase])
   done
 
 lemma subtopology_PiE:
@@ -286,10 +286,9 @@
   done
 qed
 
-
 lemma product_topology_base_alt:
    "finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
-    relative_to topspace(product_topology X I) =
+    relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i)) =
     (\<lambda>F. (\<exists>U. F =  Pi\<^sub>E I U \<and> finite {i \<in> I. U i \<noteq> topspace(X i)} \<and> (\<forall>i \<in> I. openin (X i) (U i))))"
    (is "?lhs = ?rhs")
 proof -
@@ -340,6 +339,15 @@
     by meson
 qed
 
+corollary openin_product_topology_alt:
+  "openin (product_topology X I) S \<longleftrightarrow>
+    (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
+                 (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
+  unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology
+  apply safe
+  apply (drule bspec; blast)+
+  done
+
 lemma closure_of_product_topology:
   "(product_topology X I) closure_of (PiE I S) = PiE I (\<lambda>i. (X i) closure_of (S i))"
 proof -
@@ -445,9 +453,9 @@
 
 subsubsection \<open>The basic property of the product topology is the continuity of projections:\<close>
 
-lemma continuous_on_topo_product_coordinates [simp]:
+lemma continuous_map_product_coordinates [simp]:
   assumes "i \<in> I"
-  shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"
+  shows "continuous_map (product_topology T I) (T i) (\<lambda>x. x i)"
 proof -
   {
     fix U assume "openin (T i) U"
@@ -463,14 +471,14 @@
       apply (subst *)
       using ** by auto
   }
-  then show ?thesis unfolding continuous_on_topo_def
-    by (auto simp add: assms topspace_product_topology PiE_iff)
+  then show ?thesis unfolding continuous_map_alt
+    by (auto simp add: assms PiE_iff)
 qed
 
-lemma continuous_on_topo_coordinatewise_then_product [intro]:
-  assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+lemma continuous_map_coordinatewise_then_product [intro]:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
           "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
-  shows "continuous_on_topo T1 (product_topology T I) f"
+  shows "continuous_map T1 (product_topology T I) f"
 unfolding product_topology_def
 proof (rule continuous_on_generated_topo)
   fix U assume "U \<in> {Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
@@ -479,7 +487,7 @@
   define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
   have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto
   have "(\<lambda>x. f x i)-`(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i
-    using that assms(1) by (simp add: continuous_on_topo_preimage_topspace)
+    using that assms(1) by (simp add: continuous_map_preimage_topspace)
   then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
     using that unfolding J_def by auto
   have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
@@ -497,25 +505,25 @@
     apply (subst product_topology_def[symmetric])
     apply (simp only: topspace_product_topology)
     apply (auto simp add: PiE_iff)
-    using assms unfolding continuous_on_topo_def by auto
+    using assms unfolding continuous_map_def by auto
 qed
 
-lemma continuous_on_topo_product_then_coordinatewise [intro]:
-  assumes "continuous_on_topo T1 (product_topology T I) f"
-  shows "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+lemma continuous_map_product_then_coordinatewise [intro]:
+  assumes "continuous_map T1 (product_topology T I) f"
+  shows "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
         "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
 proof -
   fix i assume "i \<in> I"
   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
-  also have "continuous_on_topo T1 (T i) (...)"
-    apply (rule continuous_on_topo_compose[of _ "product_topology T I"])
+  also have "continuous_map T1 (T i) (...)"
+    apply (rule continuous_map_compose[of _ "product_topology T I"])
     using assms \<open>i \<in> I\<close> by auto
-  ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
+  ultimately show "continuous_map T1 (T i) (\<lambda>x. f x i)"
     by simp
 next
   fix i x assume "i \<notin> I" "x \<in> topspace T1"
   have "f x \<in> topspace (product_topology T I)"
-    using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
+    using assms \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
   then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
     using topspace_product_topology by metis
   then show "f x i = undefined"
@@ -524,11 +532,11 @@
 
 lemma continuous_on_restrict:
   assumes "J \<subseteq> I"
-  shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
-proof (rule continuous_on_topo_coordinatewise_then_product)
+  shows "continuous_map (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
+proof (rule continuous_map_coordinatewise_then_product)
   fix i assume "i \<in> J"
   then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
-  then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
+  then show "continuous_map (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
     using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
 next
   fix i assume "i \<notin> J"
@@ -571,7 +579,7 @@
   have **: "finite {i. X i \<noteq> UNIV}"
     unfolding X_def V_def J_def using assms(1) by auto
   have "open (Pi\<^sub>E UNIV X)"
-    unfolding open_fun_def 
+    unfolding open_fun_def
     by (simp_all add: * ** product_topology_basis)
   moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
     apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
@@ -594,28 +602,28 @@
 
 lemma continuous_on_product_coordinates [simp]:
   "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
-  unfolding continuous_on_topo_UNIV euclidean_product_topology
-  by (rule continuous_on_topo_product_coordinates, simp)
+  using continuous_map_product_coordinates [of _ UNIV "\<lambda>i. euclidean"]
+    by (metis (no_types) continuous_map_iff_continuous euclidean_product_topology iso_tuple_UNIV_I subtopology_UNIV)
 
 lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
   fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
   assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
   shows "continuous_on S f"
-  using continuous_on_topo_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
-  by (metis UNIV_I assms continuous_on_continuous_on_topo euclidean_product_topology)
+  using continuous_map_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
+  by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology)
 
 lemma continuous_on_product_then_coordinatewise_UNIV:
   assumes "continuous_on UNIV f"
   shows "continuous_on UNIV (\<lambda>x. f x i)"
-using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
-by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
+  using assms unfolding continuous_map_iff_continuous2 [symmetric] euclidean_product_topology
+  by fastforce
 
 lemma continuous_on_product_then_coordinatewise:
   assumes "continuous_on S f"
   shows "continuous_on S (\<lambda>x. f x i)"
 proof -
   have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
-    by (metis assms continuous_on_compose continuous_on_id 
+    by (metis assms continuous_on_compose continuous_on_id
         continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
   then show ?thesis
     by auto
@@ -1582,4 +1590,166 @@
   qed
 qed
 
+subsection \<open>Open Pi-sets in the product topology\<close>
+
+proposition openin_PiE_gen:
+  "openin (product_topology X I) (PiE I S) \<longleftrightarrow>
+        PiE I S = {} \<or>
+        finite {i \<in> I. ~(S i = topspace(X i))} \<and> (\<forall>i \<in> I. openin (X i) (S i))"
+  (is "?lhs \<longleftrightarrow> _ \<or> ?rhs")
+proof (cases "PiE I S = {}")
+  case False
+  moreover have "?lhs = ?rhs"
+  proof
+    assume L: ?lhs
+    moreover
+    obtain z where z: "z \<in> PiE I S"
+      using False by blast
+    ultimately obtain U where fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
+      and "Pi\<^sub>E I U \<noteq> {}"
+      and sub: "Pi\<^sub>E I U \<subseteq> Pi\<^sub>E I S"
+      by (fastforce simp add: openin_product_topology_alt)
+    then have *: "\<And>i. i \<in> I \<Longrightarrow> U i \<subseteq> S i"
+      by (simp add: subset_PiE)
+    show ?rhs
+    proof (intro conjI ballI)
+      show "finite {i \<in> I. S i \<noteq> topspace (X i)}"
+        apply (rule finite_subset [OF _ fin], clarify)
+        using *
+        by (metis False L openin_subset topspace_product_topology subset_PiE subset_antisym)
+    next
+      fix i :: "'a"
+      assume "i \<in> I"
+      then show "openin (X i) (S i)"
+        using open_map_product_projection [of i I X] L
+        apply (simp add: open_map_def)
+        apply (drule_tac x="PiE I S" in spec)
+        apply (simp add: False image_projection_PiE split: if_split_asm)
+        done
+    qed
+  next
+    assume ?rhs
+    then show ?lhs
+      apply (simp only: openin_product_topology)
+      apply (rule arbitrary_union_of_inc)
+      apply (auto simp: product_topology_base_alt)
+      done
+  qed
+  ultimately show ?thesis
+    by simp
+qed simp
+
+
+corollary openin_PiE:
+   "finite I \<Longrightarrow> openin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. openin (X i) (S i))"
+  by (simp add: openin_PiE_gen)
+
+proposition compact_space_product_topology:
+   "compact_space(product_topology X I) \<longleftrightarrow>
+    topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. compact_space(X i))"
+    (is "?lhs = ?rhs")
+proof (cases "topspace(product_topology X I) = {}")
+  case False
+  then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
+    by auto
+  show ?thesis
+  proof
+    assume L: ?lhs
+    show ?rhs
+    proof (clarsimp simp add: False compact_space_def)
+      fix i
+      assume "i \<in> I"
+      with L have "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
+        by (simp add: continuous_map_product_projection)
+      moreover
+      have "\<And>x. x \<in> topspace (X i) \<Longrightarrow> x \<in> (\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+        using \<open>i \<in> I\<close> z
+        apply (rule_tac x="\<lambda>j. if j = i then x else if j \<in> I then z j else undefined" in image_eqI, auto)
+        done
+      then have "(\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = topspace (X i)"
+        using \<open>i \<in> I\<close> z by auto
+      ultimately show "compactin (X i) (topspace (X i))"
+        by (metis L compact_space_def image_compactin topspace_product_topology)
+    qed
+  next
+    assume R: ?rhs
+    show ?lhs
+    proof (cases "I = {}")
+      case True
+      with R show ?thesis
+        by (simp add: compact_space_def)
+    next
+      case False
+      then obtain i where "i \<in> I"
+        by blast
+      show ?thesis
+        using R
+      proof
+        assume com [rule_format]: "\<forall>i\<in>I. compact_space (X i)"
+        let ?\<C> = "{{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
+        show "compact_space (product_topology X I)"
+        proof (rule Alexander_subbase_alt)
+          show "topspace (product_topology X I) \<subseteq> \<Union>?\<C>"
+            unfolding topspace_product_topology using \<open>i \<in> I\<close> by blast
+        next
+          fix C
+          assume Csub: "C \<subseteq> ?\<C>" and UC: "topspace (product_topology X I) \<subseteq> \<Union>C"
+          define \<D> where "\<D> \<equiv> \<lambda>i. {U. openin (X i) U \<and> {f. f i \<in> U} \<in> C}"
+          show "\<exists>C'. finite C' \<and> C' \<subseteq> C \<and> topspace (product_topology X I) \<subseteq> \<Union>C'"
+          proof (cases "\<exists>i. i \<in> I \<and> topspace (X i) \<subseteq> \<Union>(\<D> i)")
+            case True
+            then obtain i where "i \<in> I"
+                   and i: "topspace (X i) \<subseteq> \<Union>(\<D> i)"
+              unfolding \<D>_def by blast
+            then have *: "\<And>\<U>. \<lbrakk>Ball \<U> (openin (X i)); topspace (X i) \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow>
+                            \<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace (X i) \<subseteq> \<Union>\<F>"
+              using com [OF \<open>i \<in> I\<close>] by (auto simp: compact_space_def compactin_def)
+            have "topspace (X i) \<subseteq> \<Union>(\<D> i)"
+              using i by auto
+            with * obtain \<F> where "finite \<F> \<and> \<F> \<subseteq> (\<D> i) \<and> topspace (X i) \<subseteq> \<Union>\<F>"
+              unfolding \<D>_def by fastforce
+            with \<open>i \<in> I\<close> show ?thesis
+              unfolding \<D>_def
+              by (rule_tac x="(\<lambda>U. {x. x i \<in> U}) ` \<F>" in exI) auto
+          next
+            case False
+            then have "\<forall>i \<in> I. \<exists>y. y \<in> topspace (X i) \<and> y \<notin> \<Union>(\<D> i)"
+              by force
+            then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> g i \<in> topspace (X i) \<and> g i \<notin> \<Union>(\<D> i)"
+              by metis
+            then have "(\<lambda>i. if i \<in> I then g i else undefined) \<in> topspace (product_topology X I)"
+              by (simp add: PiE_I)
+            moreover have "(\<lambda>i. if i \<in> I then g i else undefined) \<notin> \<Union>C"
+              using Csub g unfolding \<D>_def by force
+            ultimately show ?thesis
+              using UC by blast
+          qed
+        qed (simp add: product_topology)
+      qed (simp add: compact_space_topspace_empty)
+    qed
+  qed
+qed (simp add: compact_space_topspace_empty)
+
+corollary compactin_PiE:
+   "compactin (product_topology X I) (PiE I S) \<longleftrightarrow>
+        PiE I S = {} \<or> (\<forall>i \<in> I. compactin (X i) (S i))"
+  by (auto simp: compactin_subspace subtopology_PiE subset_PiE compact_space_product_topology
+       PiE_eq_empty_iff)
+
+lemma in_product_topology_closure_of:
+   "z \<in> (product_topology X I) closure_of S
+        \<Longrightarrow> i \<in> I \<Longrightarrow> z i \<in> ((X i) closure_of ((\<lambda>x. x i) ` S))"
+  using continuous_map_product_projection
+  by (force simp: continuous_map_eq_image_closure_subset image_subset_iff)
+
+lemma homeomorphic_space_singleton_product:
+   "product_topology X {k} homeomorphic_space (X k)"
+  unfolding homeomorphic_space
+  apply (rule_tac x="\<lambda>x. x k" in exI)
+  apply (rule bijective_open_imp_homeomorphic_map)
+     apply (simp_all add: continuous_map_product_projection open_map_product_projection)
+  unfolding PiE_over_singleton_iff
+   apply (auto simp: image_iff inj_on_def)
+  done
+
 end
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -1,4 +1,4 @@
-subsection \<open>Ordered Euclidean Space\<close> (* why not Section? *)
+section \<open>Ordered Euclidean Space\<close>
 
 theory Ordered_Euclidean_Space
 imports
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -135,6 +135,9 @@
 
 subsection%unimportant\<open>Basic lemmas about paths\<close>
 
+lemma pathin_iff_path_real [simp]: "pathin euclideanreal g \<longleftrightarrow> path g"
+  by (simp add: pathin_def path_def)
+
 lemma continuous_on_path: "path f \<Longrightarrow> t \<subseteq> {0..1} \<Longrightarrow> continuous_on t f"
   using continuous_on_subset path_def by blast
 
@@ -1468,7 +1471,7 @@
 lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y"
   unfolding path_component_def by auto
 
-lemma path_connected_linepath:
+lemma path_component_linepath:
     fixes s :: "'a::real_normed_vector set"
     shows "closed_segment a b \<subseteq> s \<Longrightarrow> path_component s a b"
   unfolding path_component_def
@@ -1502,6 +1505,10 @@
 definition%important "path_connected s \<longleftrightarrow>
   (\<forall>x\<in>s. \<forall>y\<in>s. \<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
 
+lemma path_connectedin_iff_path_connected_real [simp]:
+     "path_connectedin euclideanreal S \<longleftrightarrow> path_connected S"
+  by (simp add: path_connectedin path_connected_def path_defs)
+
 lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
   unfolding path_connected_def path_component_def by auto
 
@@ -1818,6 +1825,29 @@
 lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
   by (simp add: convex_imp_path_connected is_interval_convex)
 
+lemma path_connectedin_path_image:
+  assumes "pathin X g" shows "path_connectedin X (g ` ({0..1}))"
+  unfolding pathin_def
+proof (rule path_connectedin_continuous_map_image)
+  show "continuous_map (subtopology euclideanreal {0..1}) X g"
+    using assms pathin_def by blast
+qed (auto simp: is_interval_1 is_interval_path_connected)
+
+lemma path_connected_space_subconnected:
+     "path_connected_space X \<longleftrightarrow>
+      (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. \<exists>S. path_connectedin X S \<and> x \<in> S \<and> y \<in> S)"
+  unfolding path_connected_space_def Ball_def
+  apply (intro all_cong1 imp_cong refl, safe)
+  using path_connectedin_path_image apply fastforce
+  by (meson path_connectedin)
+
+lemma connectedin_path_image: "pathin X g \<Longrightarrow> connectedin X (g ` ({0..1}))"
+  by (simp add: path_connectedin_imp_connectedin path_connectedin_path_image)
+
+lemma compactin_path_image: "pathin X g \<Longrightarrow> compactin X (g ` ({0..1}))"
+  unfolding pathin_def
+  by (rule image_compactin [of "top_of_set {0..1}"]) auto
+
 lemma linear_homeomorphism_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "linear f" "inj f"
@@ -1935,6 +1965,372 @@
 qed
 
 
+subsection\<open>Path components\<close>
+
+definition path_component_of
+  where "path_component_of X x y \<equiv> \<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y"
+
+abbreviation path_component_of_set
+  where "path_component_of_set X x \<equiv> Collect (path_component_of X x)"
+
+definition path_components_of :: "'a topology \<Rightarrow> 'a set set"
+  where "path_components_of X \<equiv> path_component_of_set X ` topspace X"
+
+lemma path_component_in_topspace:
+   "path_component_of X x y \<Longrightarrow> x \<in> topspace X \<and> y \<in> topspace X"
+  by (auto simp: path_component_of_def pathin_def continuous_map_def)
+
+lemma path_component_of_refl:
+   "path_component_of X x x \<longleftrightarrow> x \<in> topspace X"
+  apply (auto simp: path_component_in_topspace)
+  apply (force simp: path_component_of_def pathin_const)
+  done
+
+lemma path_component_of_sym:
+  assumes "path_component_of X x y"
+  shows "path_component_of X y x"
+  using assms
+  apply (clarsimp simp: path_component_of_def pathin_def)
+  apply (rule_tac x="g \<circ> (\<lambda>t. 1 - t)" in exI)
+  apply (auto intro!: continuous_map_compose)
+  apply (force simp: continuous_map_in_subtopology continuous_on_op_minus)
+  done
+
+lemma path_component_of_sym_iff:
+   "path_component_of X x y \<longleftrightarrow> path_component_of X y x"
+  by (metis path_component_of_sym)
+
+lemma path_component_of_trans:
+  assumes "path_component_of X x y" and "path_component_of X y z"
+  shows "path_component_of X x z"
+  unfolding path_component_of_def pathin_def
+proof -
+  let ?T01 = "top_of_set {0..1::real}"
+  obtain g1 g2 where g1: "continuous_map ?T01 X g1" "x = g1 0" "y = g1 1"
+    and g2: "continuous_map ?T01 X g2" "g2 0 = g1 1" "z = g2 1"
+    using assms unfolding path_component_of_def pathin_def by blast
+  let ?g = "\<lambda>x. if x \<le> 1/2 then (g1 \<circ> (\<lambda>t. 2 * t)) x else (g2 \<circ> (\<lambda>t. 2 * t -1)) x"
+  show "\<exists>g. continuous_map ?T01 X g \<and> g 0 = x \<and> g 1 = z"
+  proof (intro exI conjI)
+    show "continuous_map (subtopology euclideanreal {0..1}) X ?g"
+    proof (intro continuous_map_cases_le continuous_map_compose, force, force)
+      show "continuous_map (subtopology ?T01 {x \<in> topspace ?T01. x \<le> 1/2}) ?T01 ((*) 2)"
+        by (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology)
+      have "continuous_map
+             (subtopology (top_of_set {0..1}) {x. 0 \<le> x \<and> x \<le> 1 \<and> 1 \<le> x * 2})
+             euclideanreal (\<lambda>t. 2 * t - 1)"
+        by (intro continuous_intros) (force intro: continuous_map_from_subtopology)
+      then show "continuous_map (subtopology ?T01 {x \<in> topspace ?T01. 1/2 \<le> x}) ?T01 (\<lambda>t. 2 * t - 1)"
+        by (force simp: continuous_map_in_subtopology)
+      show "(g1 \<circ> (*) 2) x = (g2 \<circ> (\<lambda>t. 2 * t - 1)) x" if "x \<in> topspace ?T01" "x = 1/2" for x
+        using that by (simp add: g2(2) mult.commute continuous_map_from_subtopology)
+    qed (auto simp: g1 g2)
+  qed (auto simp: g1 g2)
+qed
+
+
+lemma path_component_of_mono:
+   "\<lbrakk>path_component_of (subtopology X S) x y; S \<subseteq> T\<rbrakk> \<Longrightarrow> path_component_of (subtopology X T) x y"
+  unfolding path_component_of_def
+  by (metis subsetD pathin_subtopology)
+
+
+lemma path_component_of:
+  "path_component_of X x y \<longleftrightarrow> (\<exists>T. path_connectedin X T \<and> x \<in> T \<and> y \<in> T)"
+  apply (auto simp: path_component_of_def)
+  using path_connectedin_path_image apply fastforce
+  apply (metis path_connectedin)
+  done
+
+lemma path_component_of_set:
+   "path_component_of X x y \<longleftrightarrow> (\<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y)"
+  by (auto simp: path_component_of_def)
+
+lemma path_component_of_subset_topspace:
+   "Collect(path_component_of X x) \<subseteq> topspace X"
+  using path_component_in_topspace by fastforce
+
+lemma path_component_of_eq_empty:
+   "Collect(path_component_of X x) = {} \<longleftrightarrow> (x \<notin> topspace X)"
+  using path_component_in_topspace path_component_of_refl by fastforce
+
+lemma path_connected_space_iff_path_component:
+   "path_connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. path_component_of X x y)"
+  by (simp add: path_component_of path_connected_space_subconnected)
+
+lemma path_connected_space_imp_path_component_of:
+   "\<lbrakk>path_connected_space X; a \<in> topspace X; b \<in> topspace X\<rbrakk>
+        \<Longrightarrow> path_component_of X a b"
+  by (simp add: path_connected_space_iff_path_component)
+
+lemma path_connected_space_path_component_set:
+   "path_connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. Collect(path_component_of X x) = topspace X)"
+  using path_component_of_subset_topspace path_connected_space_iff_path_component by fastforce
+
+lemma path_component_of_maximal:
+   "\<lbrakk>path_connectedin X s; x \<in> s\<rbrakk> \<Longrightarrow> s \<subseteq> Collect(path_component_of X x)"
+  using path_component_of by fastforce
+
+lemma path_component_of_equiv:
+   "path_component_of X x y \<longleftrightarrow> x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x = path_component_of X y"
+    (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    apply (simp add: fun_eq_iff path_component_in_topspace)
+    apply (meson path_component_of_sym path_component_of_trans)
+    done
+qed (simp add: path_component_of_refl)
+
+lemma path_component_of_disjoint:
+     "disjnt (Collect (path_component_of X x)) (Collect (path_component_of X y)) \<longleftrightarrow>
+      ~(path_component_of X x y)"
+  by (force simp: disjnt_def path_component_of_eq_empty path_component_of_equiv)
+
+lemma path_component_of_eq:
+   "path_component_of X x = path_component_of X y \<longleftrightarrow>
+        (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
+        x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x y"
+  by (metis Collect_empty_eq_bot path_component_of_eq_empty path_component_of_equiv)
+
+lemma path_connectedin_path_component_of:
+  "path_connectedin X (Collect (path_component_of X x))"
+proof -
+  have "\<And>y. path_component_of X x y
+        \<Longrightarrow> path_component_of (subtopology X (Collect (path_component_of X x))) x y"
+    by (meson path_component_of path_component_of_maximal path_connectedin_subtopology)
+  then show ?thesis
+    apply (simp add: path_connectedin_def path_component_of_subset_topspace path_connected_space_iff_path_component)
+    by (metis Int_absorb1 mem_Collect_eq path_component_of_equiv path_component_of_subset_topspace topspace_subtopology)
+qed
+
+lemma Union_path_components_of:
+     "\<Union>(path_components_of X) = topspace X"
+  by (auto simp: path_components_of_def path_component_of_equiv)
+
+lemma path_components_of_maximal:
+   "\<lbrakk>C \<in> path_components_of X; path_connectedin X S; ~disjnt C S\<rbrakk> \<Longrightarrow> S \<subseteq> C"
+  apply (auto simp: path_components_of_def path_component_of_equiv)
+  using path_component_of_maximal path_connectedin_def apply fastforce
+  by (meson disjnt_subset2 path_component_of_disjoint path_component_of_equiv path_component_of_maximal)
+
+lemma pairwise_disjoint_path_components_of:
+     "pairwise disjnt (path_components_of X)"
+  by (auto simp: path_components_of_def pairwise_def path_component_of_disjoint path_component_of_equiv)
+
+lemma complement_path_components_of_Union:
+   "C \<in> path_components_of X
+        \<Longrightarrow> topspace X - C = \<Union>(path_components_of X - {C})"
+  by (metis Diff_cancel Diff_subset Union_path_components_of cSup_singleton diff_Union_pairwise_disjoint insert_subset pairwise_disjoint_path_components_of)
+
+lemma nonempty_path_components_of:
+  "C \<in> path_components_of X \<Longrightarrow> (C \<noteq> {})"
+  apply (clarsimp simp: path_components_of_def path_component_of_eq_empty)
+  by (meson path_component_of_refl)
+
+lemma path_components_of_subset: "C \<in> path_components_of X \<Longrightarrow> C \<subseteq> topspace X"
+  by (auto simp: path_components_of_def path_component_of_equiv)
+
+lemma path_connectedin_path_components_of:
+   "C \<in> path_components_of X \<Longrightarrow> path_connectedin X C"
+  by (auto simp: path_components_of_def path_connectedin_path_component_of)
+
+lemma path_component_in_path_components_of:
+  "Collect (path_component_of X a) \<in> path_components_of X \<longleftrightarrow> a \<in> topspace X"
+  apply (rule iffI)
+  using nonempty_path_components_of path_component_of_eq_empty apply fastforce
+  by (simp add: path_components_of_def)
+
+lemma path_connectedin_Union:
+  assumes \<A>: "\<And>S. S \<in> \<A> \<Longrightarrow> path_connectedin X S" "\<Inter>\<A> \<noteq> {}"
+  shows "path_connectedin X (\<Union>\<A>)"
+proof -
+  obtain a where "\<And>S. S \<in> \<A> \<Longrightarrow> a \<in> S"
+    using assms by blast
+  then have "\<And>x. x \<in> topspace (subtopology X (\<Union>\<A>)) \<Longrightarrow> path_component_of (subtopology X (\<Union>\<A>)) a x"
+    apply (simp add: topspace_subtopology)
+    by (meson Union_upper \<A> path_component_of path_connectedin_subtopology)
+  then show ?thesis
+    using \<A> unfolding path_connectedin_def
+    by (metis Sup_le_iff path_component_of_equiv path_connected_space_iff_path_component)
+qed
+
+lemma path_connectedin_Un:
+   "\<lbrakk>path_connectedin X S; path_connectedin X T; S \<inter> T \<noteq> {}\<rbrakk>
+    \<Longrightarrow> path_connectedin X (S \<union> T)"
+  by (blast intro: path_connectedin_Union [of "{S,T}", simplified])
+
+lemma path_connected_space_iff_components_eq:
+  "path_connected_space X \<longleftrightarrow>
+    (\<forall>C \<in> path_components_of X. \<forall>C' \<in> path_components_of X. C = C')"
+  unfolding path_components_of_def
+proof (intro iffI ballI)
+  assume "\<forall>C \<in> path_component_of_set X ` topspace X.
+             \<forall>C' \<in> path_component_of_set X ` topspace X. C = C'"
+  then show "path_connected_space X"
+    using path_component_of_refl path_connected_space_iff_path_component by fastforce
+qed (auto simp: path_connected_space_path_component_set)
+
+lemma path_components_of_eq_empty:
+   "path_components_of X = {} \<longleftrightarrow> topspace X = {}"
+  using Union_path_components_of nonempty_path_components_of by fastforce
+
+lemma path_components_of_empty_space:
+   "topspace X = {} \<Longrightarrow> path_components_of X = {}"
+  by (simp add: path_components_of_eq_empty)
+
+lemma path_components_of_subset_singleton:
+  "path_components_of X \<subseteq> {S} \<longleftrightarrow>
+        path_connected_space X \<and> (topspace X = {} \<or> topspace X = S)"
+proof (cases "topspace X = {}")
+  case True
+  then show ?thesis
+    by (auto simp: path_components_of_empty_space path_connected_space_topspace_empty)
+next
+  case False
+  have "(path_components_of X = {S}) \<longleftrightarrow> (path_connected_space X \<and> topspace X = S)"
+  proof (intro iffI conjI)
+    assume L: "path_components_of X = {S}"
+    then show "path_connected_space X"
+      by (simp add: path_connected_space_iff_components_eq)
+    show "topspace X = S"
+      by (metis L ccpo_Sup_singleton [of S] Union_path_components_of)
+  next
+    assume R: "path_connected_space X \<and> topspace X = S"
+    then show "path_components_of X = {S}"
+      using ccpo_Sup_singleton [of S]
+      by (metis False all_not_in_conv insert_iff mk_disjoint_insert path_component_in_path_components_of path_connected_space_iff_components_eq path_connected_space_path_component_set)
+  qed
+  with False show ?thesis
+    by (simp add: path_components_of_eq_empty subset_singleton_iff)
+qed
+
+lemma path_connected_space_iff_components_subset_singleton:
+   "path_connected_space X \<longleftrightarrow> (\<exists>a. path_components_of X \<subseteq> {a})"
+  by (simp add: path_components_of_subset_singleton)
+
+lemma path_components_of_eq_singleton:
+   "path_components_of X = {S} \<longleftrightarrow> path_connected_space X \<and> topspace X \<noteq> {} \<and> S = topspace X"
+  by (metis cSup_singleton insert_not_empty path_components_of_subset_singleton subset_singleton_iff)
+
+lemma path_components_of_path_connected_space:
+   "path_connected_space X \<Longrightarrow> path_components_of X = (if topspace X = {} then {} else {topspace X})"
+  by (simp add: path_components_of_eq_empty path_components_of_eq_singleton)
+
+lemma path_component_subset_connected_component_of:
+   "path_component_of_set X x \<subseteq> connected_component_of_set X x"
+proof (cases "x \<in> topspace X")
+  case True
+  then show ?thesis
+    by (simp add: connected_component_of_maximal path_component_of_refl path_connectedin_imp_connectedin path_connectedin_path_component_of)
+next
+  case False
+  then show ?thesis
+    using path_component_of_eq_empty by fastforce
+qed
+
+lemma exists_path_component_of_superset:
+  assumes S: "path_connectedin X S" and ne: "topspace X \<noteq> {}"
+  obtains C where "C \<in> path_components_of X" "S \<subseteq> C"
+proof (cases "S = {}")
+  case True
+  then show ?thesis
+    using ne path_components_of_eq_empty that by fastforce
+next
+  case False
+  then obtain a where "a \<in> S"
+    by blast
+  show ?thesis
+  proof
+    show "Collect (path_component_of X a) \<in> path_components_of X"
+      by (meson \<open>a \<in> S\<close> S subsetD path_component_in_path_components_of path_connectedin_subset_topspace)
+    show "S \<subseteq> Collect (path_component_of X a)"
+      by (simp add: S \<open>a \<in> S\<close> path_component_of_maximal)
+  qed
+qed
+
+lemma path_component_of_eq_overlap:
+   "path_component_of X x = path_component_of X y \<longleftrightarrow>
+      (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
+      Collect (path_component_of X x) \<inter> Collect (path_component_of X y) \<noteq> {}"
+  by (metis disjnt_def empty_iff inf_bot_right mem_Collect_eq path_component_of_disjoint path_component_of_eq path_component_of_eq_empty)
+
+lemma path_component_of_nonoverlap:
+   "Collect (path_component_of X x) \<inter> Collect (path_component_of X y) = {} \<longleftrightarrow>
+    (x \<notin> topspace X) \<or> (y \<notin> topspace X) \<or>
+    path_component_of X x \<noteq> path_component_of X y"
+  by (metis inf.idem path_component_of_eq_empty path_component_of_eq_overlap)
+
+lemma path_component_of_overlap:
+   "Collect (path_component_of X x) \<inter> Collect (path_component_of X y) \<noteq> {} \<longleftrightarrow>
+    x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x = path_component_of X y"
+  by (meson path_component_of_nonoverlap)
+
+lemma path_components_of_disjoint:
+     "\<lbrakk>C \<in> path_components_of X; C' \<in> path_components_of X\<rbrakk> \<Longrightarrow> disjnt C C' \<longleftrightarrow> C \<noteq> C'"
+  by (auto simp: path_components_of_def path_component_of_disjoint path_component_of_equiv)
+
+lemma path_components_of_overlap:
+    "\<lbrakk>C \<in> path_components_of X; C' \<in> path_components_of X\<rbrakk> \<Longrightarrow> C \<inter> C' \<noteq> {} \<longleftrightarrow> C = C'"
+  by (auto simp: path_components_of_def path_component_of_equiv)
+
+lemma path_component_of_unique:
+   "\<lbrakk>x \<in> C; path_connectedin X C; \<And>C'. \<lbrakk>x \<in> C'; path_connectedin X C'\<rbrakk> \<Longrightarrow> C' \<subseteq> C\<rbrakk>
+        \<Longrightarrow> Collect (path_component_of X x) = C"
+  by (meson subsetD eq_iff path_component_of_maximal path_connectedin_path_component_of)
+
+lemma path_component_of_discrete_topology [simp]:
+  "Collect (path_component_of (discrete_topology U) x) = (if x \<in> U then {x} else {})"
+proof -
+  have "\<And>C'. \<lbrakk>x \<in> C'; path_connectedin (discrete_topology U) C'\<rbrakk> \<Longrightarrow> C' \<subseteq> {x}"
+    by (metis path_connectedin_discrete_topology subsetD singletonD)
+  then have "x \<in> U \<Longrightarrow> Collect (path_component_of (discrete_topology U) x) = {x}"
+    by (simp add: path_component_of_unique)
+  then show ?thesis
+    using path_component_in_topspace by fastforce
+qed
+
+lemma path_component_of_discrete_topology_iff [simp]:
+  "path_component_of (discrete_topology U) x y \<longleftrightarrow> x \<in> U \<and> y=x"
+  by (metis empty_iff insertI1 mem_Collect_eq path_component_of_discrete_topology singletonD)
+
+lemma path_components_of_discrete_topology [simp]:
+   "path_components_of (discrete_topology U) = (\<lambda>x. {x}) ` U"
+  by (auto simp: path_components_of_def image_def fun_eq_iff)
+
+lemma homeomorphic_map_path_component_of:
+  assumes f: "homeomorphic_map X Y f" and x: "x \<in> topspace X"
+  shows "Collect (path_component_of Y (f x)) = f ` Collect(path_component_of X x)"
+proof -
+  obtain g where g: "homeomorphic_maps X Y f g"
+    using f homeomorphic_map_maps by blast
+  show ?thesis
+  proof
+    have "Collect (path_component_of Y (f x)) \<subseteq> topspace Y"
+      by (simp add: path_component_of_subset_topspace)
+    moreover have "g ` Collect(path_component_of Y (f x)) \<subseteq> Collect (path_component_of X (g (f x)))"
+      using g x unfolding homeomorphic_maps_def
+      by (metis f homeomorphic_imp_surjective_map imageI mem_Collect_eq path_component_of_maximal path_component_of_refl path_connectedin_continuous_map_image path_connectedin_path_component_of)
+    ultimately show "Collect (path_component_of Y (f x)) \<subseteq> f ` Collect (path_component_of X x)"
+      using g x unfolding homeomorphic_maps_def continuous_map_def image_iff subset_iff
+      by metis
+    show "f ` Collect (path_component_of X x) \<subseteq> Collect (path_component_of Y (f x))"
+    proof (rule path_component_of_maximal)
+      show "path_connectedin Y (f ` Collect (path_component_of X x))"
+        by (meson f homeomorphic_map_path_connectedness_eq path_connectedin_path_component_of)
+    qed (simp add: path_component_of_refl x)
+  qed
+qed
+
+lemma homeomorphic_map_path_components_of:
+  assumes "homeomorphic_map X Y f"
+  shows "path_components_of Y = (image f) ` (path_components_of X)"
+  unfolding path_components_of_def homeomorphic_imp_surjective_map [OF assms, symmetric]
+  apply safe
+  using assms homeomorphic_map_path_component_of apply fastforce
+  by (metis assms homeomorphic_map_path_component_of imageI)
+
+
 subsection \<open>Sphere is path-connected\<close>
 
 lemma path_connected_punctured_universe:
@@ -2078,7 +2474,7 @@
         done
     }
     then have pcx: "path_component (- s) x (a + C *\<^sub>R (x - a))"
-      by (force simp: closed_segment_def intro!: path_connected_linepath)
+      by (force simp: closed_segment_def intro!: path_component_linepath)
     define D where "D = B / norm(y - a)"  \<comment> \<open>massive duplication with the proof above\<close>
     { fix u
       assume u: "(1 - u) *\<^sub>R y + u *\<^sub>R (a + D *\<^sub>R (y - a)) \<in> s" and "0 \<le> u" "u \<le> 1"
@@ -2113,7 +2509,7 @@
         done
     }
     then have pdy: "path_component (- s) y (a + D *\<^sub>R (y - a))"
-      by (force simp: closed_segment_def intro!: path_connected_linepath)
+      by (force simp: closed_segment_def intro!: path_component_linepath)
     have pyx: "path_component (- s) (a + D *\<^sub>R (y - a)) (a + C *\<^sub>R (x - a))"
       apply (rule path_component_of_subset [of "sphere a B"])
        using \<open>s \<subseteq> ball a B\<close>
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Analysis/Product_Topology.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -1,15 +1,12 @@
+section\<open>The binary product topology\<close>
+
 theory Product_Topology
 imports Function_Topology   
 begin
 
-lemma subset_UnE: (*FIXME MOVE*)
-  assumes "C \<subseteq> A \<union> B"
-    obtains A' B' where "A' \<subseteq> A" "B' \<subseteq> B" "C = A' \<union> B'"
-  by (metis assms Int_Un_distrib inf.order_iff inf_le2)
-
 section \<open>Product Topology\<close> 
 
-subsection\<open>A binary product topology where the two types can be different.\<close>
+subsection\<open>Definition\<close>
 
 definition prod_topology :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<times> 'b) topology" where
  "prod_topology X Y \<equiv> topology (arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T}))"
@@ -34,7 +31,7 @@
 proof (rule topology_inverse')
   show "istopology (arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T}))"
     apply (rule istopology_base, simp)
-    by (metis openin_Int times_Int_times)
+    by (metis openin_Int Times_Int_Times)
 qed
 
 lemma topspace_prod_topology [simp]:
@@ -62,7 +59,7 @@
 proof -
   have "((\<lambda>U. \<exists>S T. U = S \<times> T \<and> openin X S \<and> openin Y T) relative_to S \<times> T) =
         (\<lambda>U. \<exists>S' T'. U = S' \<times> T' \<and> (openin X relative_to S) S' \<and> (openin Y relative_to T) T')"
-    by (auto simp: relative_to_def times_Int_times fun_eq_iff) metis
+    by (auto simp: relative_to_def Times_Int_Times fun_eq_iff) metis
   then show ?thesis
     by (simp add: topology_eq openin_prod_topology arbitrary_union_of_relative_to flip: openin_relative_to)
 qed
@@ -81,7 +78,7 @@
 
 lemma prod_topology_subtopology_eu [simp]:
   "prod_topology (subtopology euclidean S) (subtopology euclidean T) = subtopology euclidean (S \<times> T)"
-  by (simp add: prod_topology_subtopology subtopology_subtopology times_Int_times)
+  by (simp add: prod_topology_subtopology subtopology_subtopology Times_Int_Times)
 
 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"
@@ -128,6 +125,29 @@
    "closedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> closedin X S \<and> closedin Y T"
   by (auto simp: closure_of_Times times_eq_iff simp flip: closure_of_eq)
 
+lemma interior_of_Times: "(prod_topology X Y) interior_of (S \<times> T) = (X interior_of S) \<times> (Y interior_of T)"
+proof (rule interior_of_unique)
+  show "(X interior_of S) \<times> Y interior_of T \<subseteq> S \<times> T"
+    by (simp add: Sigma_mono interior_of_subset)
+  show "openin (prod_topology X Y) ((X interior_of S) \<times> Y interior_of T)"
+    by (simp add: openin_Times)
+next
+  show "T' \<subseteq> (X interior_of S) \<times> Y interior_of T" if "T' \<subseteq> S \<times> T" "openin (prod_topology X Y) T'" for T'
+  proof (clarsimp; intro conjI)
+    fix a :: "'a" and b :: "'b"
+    assume "(a, b) \<in> T'"
+    with that obtain U V where UV: "openin X U" "openin Y V" "a \<in> U" "b \<in> V" "U \<times> V \<subseteq> T'"
+      by (metis openin_prod_topology_alt)
+    then show "a \<in> X interior_of S"
+      using interior_of_maximal_eq that(1) by fastforce
+    show "b \<in> Y interior_of T"
+      using UV interior_of_maximal_eq that(1)
+      by (metis SigmaI mem_Sigma_iff subset_eq)
+  qed
+qed
+
+subsection \<open>Continuity\<close>
+
 lemma continuous_map_pairwise:
    "continuous_map Z (prod_topology X Y) f \<longleftrightarrow> continuous_map Z X (fst \<circ> f) \<and> continuous_map Z Y (snd \<circ> f)"
    (is "?lhs = ?rhs")
@@ -297,37 +317,6 @@
     by (simp add: continuous_map_paired case_prod_unfold continuous_map_of_fst [unfolded o_def] continuous_map_of_snd [unfolded o_def])
 qed
 
-lemma homeomorphic_maps_prod:
-   "homeomorphic_maps (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y)) (\<lambda>(x,y). (f' x, g' y)) \<longleftrightarrow>
-        topspace(prod_topology X Y) = {} \<and>
-        topspace(prod_topology X' Y') = {} \<or>
-        homeomorphic_maps X X' f f' \<and>
-        homeomorphic_maps Y Y' g g'"
-  unfolding homeomorphic_maps_def continuous_map_prod_top
-  by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
-
-lemma embedding_map_graph:
-   "embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
-    (is "?lhs = ?rhs")
-proof
-  assume L: ?lhs
-  have "snd \<circ> (\<lambda>x. (x, f x)) = f"
-    by force
-  moreover have "continuous_map X Y (snd \<circ> (\<lambda>x. (x, f x)))"
-    using L
-    unfolding embedding_map_def
-    by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map)
-  ultimately show ?rhs
-    by simp
-next
-  assume R: ?rhs
-  then show ?lhs
-    unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def
-    by (rule_tac x=fst in exI)
-       (auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology
-                   continuous_map_fst topspace_subtopology)
-qed
-
 lemma in_prod_topology_closure_of:
   assumes  "z \<in> (prod_topology X Y) closure_of S"
   shows "fst z \<in> X closure_of (fst ` S)" "snd z \<in> Y closure_of (snd ` S)"
@@ -412,7 +401,7 @@
           then show ?case
             unfolding \<X>_def \<Y>_def
             apply (simp add: Int_ac subset_eq image_def)
-            apply (metis (no_types) openin_Int openin_topspace times_Int_times)
+            apply (metis (no_types) openin_Int openin_topspace Times_Int_Times)
             done
         qed auto
         then show ?thesis
@@ -450,10 +439,85 @@
     using False by blast
 qed
 
-
 lemma compactin_Times:
    "compactin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> compactin X S \<and> compactin Y T"
   by (auto simp: compactin_subspace subtopology_Times compact_space_prod_topology)
 
+subsection\<open>Homeomorphic maps\<close>
+
+lemma homeomorphic_maps_prod:
+   "homeomorphic_maps (prod_topology X Y) (prod_topology X' Y') (\<lambda>(x,y). (f x, g y)) (\<lambda>(x,y). (f' x, g' y)) \<longleftrightarrow>
+        topspace(prod_topology X Y) = {} \<and>
+        topspace(prod_topology X' Y') = {} \<or>
+        homeomorphic_maps X X' f f' \<and>
+        homeomorphic_maps Y Y' g g'"
+  unfolding homeomorphic_maps_def continuous_map_prod_top
+  by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
+
+lemma embedding_map_graph:
+   "embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
+    (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  have "snd \<circ> (\<lambda>x. (x, f x)) = f"
+    by force
+  moreover have "continuous_map X Y (snd \<circ> (\<lambda>x. (x, f x)))"
+    using L
+    unfolding embedding_map_def
+    by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map)
+  ultimately show ?rhs
+    by simp
+next
+  assume R: ?rhs
+  then show ?lhs
+    unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def
+    by (rule_tac x=fst in exI)
+       (auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology
+                   continuous_map_fst topspace_subtopology)
+qed
+
+lemma homeomorphic_space_prod_topology:
+   "\<lbrakk>X homeomorphic_space X''; Y homeomorphic_space Y'\<rbrakk>
+        \<Longrightarrow> prod_topology X Y homeomorphic_space prod_topology X'' Y'"
+using homeomorphic_maps_prod unfolding homeomorphic_space_def by blast
+
+lemma prod_topology_homeomorphic_space_left:
+   "topspace Y = {b} \<Longrightarrow> prod_topology X Y homeomorphic_space X"
+  unfolding homeomorphic_space_def
+  by (rule_tac x=fst in exI) (simp add: homeomorphic_map_def inj_on_def flip: homeomorphic_map_maps)
+
+lemma prod_topology_homeomorphic_space_right:
+   "topspace X = {a} \<Longrightarrow> prod_topology X Y homeomorphic_space Y"
+  unfolding homeomorphic_space_def
+  by (rule_tac x=snd in exI) (simp add: homeomorphic_map_def inj_on_def flip: homeomorphic_map_maps)
+
+
+lemma homeomorphic_space_prod_topology_sing1:
+     "b \<in> topspace Y \<Longrightarrow> X homeomorphic_space (prod_topology X (subtopology Y {b}))"
+  by (metis empty_subsetI homeomorphic_space_sym inf.absorb_iff2 insert_subset prod_topology_homeomorphic_space_left topspace_subtopology)
+
+lemma homeomorphic_space_prod_topology_sing2:
+     "a \<in> topspace X \<Longrightarrow> Y homeomorphic_space (prod_topology (subtopology X {a}) Y)"
+  by (metis empty_subsetI homeomorphic_space_sym inf.absorb_iff2 insert_subset prod_topology_homeomorphic_space_right topspace_subtopology)
+
+lemma topological_property_of_prod_component:
+  assumes major: "P(prod_topology X Y)"
+    and X: "\<And>x. \<lbrakk>x \<in> topspace X; P(prod_topology X Y)\<rbrakk> \<Longrightarrow> P(subtopology (prod_topology X Y) ({x} \<times> topspace Y))"
+    and Y: "\<And>y. \<lbrakk>y \<in> topspace Y; P(prod_topology X Y)\<rbrakk> \<Longrightarrow> P(subtopology (prod_topology X Y) (topspace X \<times> {y}))"
+    and PQ:  "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
+    and PR: "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> R X')"
+  shows "topspace(prod_topology X Y) = {} \<or> Q X \<and> R Y"
+proof -
+  have "Q X \<and> R Y" if "topspace(prod_topology X Y) \<noteq> {}"
+  proof -
+    from that obtain a b where a: "a \<in> topspace X" and b: "b \<in> topspace Y"
+      by force
+    show ?thesis
+      using X [OF a major] and Y [OF b major] homeomorphic_space_prod_topology_sing1 [OF b, of X] homeomorphic_space_prod_topology_sing2 [OF a, of Y]
+      by (simp add: subtopology_Times) (meson PQ PR homeomorphic_space_prod_topology_sing2 homeomorphic_space_sym)
+  qed
+  then show ?thesis by metis
+qed
+
 end
 
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -1,7 +1,7 @@
 section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
 
 theory T1_Spaces
-imports Function_Topology 
+imports Product_Topology 
 begin
 
 definition t1_space where
@@ -198,4 +198,20 @@
     using False by blast
 qed
 
+lemma t1_space_prod_topology:
+   "t1_space(prod_topology X Y) \<longleftrightarrow> topspace(prod_topology X Y) = {} \<or> t1_space X \<and> t1_space Y"
+proof (cases "topspace (prod_topology X Y) = {}")
+  case True then show ?thesis
+  by (auto simp: t1_space_empty)
+next
+  case False
+  have eq: "{(x,y)} = {x} \<times> {y}" for x y
+    by simp
+  have "t1_space (prod_topology X Y) \<longleftrightarrow> (t1_space X \<and> t1_space Y)"
+    using False
+    by (force simp: t1_space_closedin_singleton closedin_Times eq simp del: insert_Times_insert)
+  with False show ?thesis
+    by simp
+qed
+
 end
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Library/FuncSet.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -550,6 +550,11 @@
 lemma PiE_eq_singleton: "(\<Pi>\<^sub>E i\<in>I. S i) = {\<lambda>i\<in>I. f i} \<longleftrightarrow> (\<forall>i\<in>I. S i = {f i})"
   by (metis (mono_tags, lifting) PiE_eq PiE_singleton insert_not_empty restrict_apply' restrict_extensional)
 
+lemma PiE_over_singleton_iff: "(\<Pi>\<^sub>E x\<in>{a}. B x) = (\<Union>b \<in> B a. {\<lambda>x \<in> {a}. b})"
+  apply (auto simp: PiE_iff split: if_split_asm)
+  apply (metis (no_types, lifting) extensionalityI restrict_apply' restrict_extensional singletonD)
+  done
+
 lemma all_PiE_elements:
    "(\<forall>z \<in> PiE I S. \<forall>i \<in> I. P i (z i)) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. \<forall>x \<in> S i. P i x)" (is "?lhs = ?rhs")
 proof (cases "PiE I S = {}")
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Product_Type.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -1134,7 +1134,7 @@
     by (cases "f x") (auto split: prod.split)
 qed
 
-lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
+lemma Times_Int_Times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
   by auto
 
 lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A"
diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Set.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -1354,6 +1354,13 @@
 lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
   by blast
 
+lemma subset_UnE: 
+  assumes "C \<subseteq> A \<union> B"
+  obtains A' B' where "A' \<subseteq> A" "B' \<subseteq> B" "C = A' \<union> B'"
+proof
+  show "C \<inter> A \<subseteq> A" "C \<inter> B \<subseteq> B" "C = (C \<inter> A) \<union> (C \<inter> B)"
+    using assms by blast+
+qed
 
 text \<open>\<^medskip> Set complement\<close>
 
@@ -1594,6 +1601,9 @@
   "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
   by auto
 
+lemma ex_image_cong_iff [simp, no_atp]:
+  "(\<exists>x. x\<in>f`A) \<longleftrightarrow> A \<noteq> {}" "(\<exists>x. x\<in>f`A \<and> P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
+  by auto
 
 subsubsection \<open>Monotonicity of various operations\<close>