new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
authorpaulson <lp15@cam.ac.uk>
Thu Mar 21 14:18:22 2019 +0000 (4 weeks ago)
changeset 69939812ce526da33
parent 69933 c15ee153dec1
child 69940 d043ccb998ee
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Abstract_Topology_2.thy
src/HOL/Analysis/Binary_Product_Measure.thy
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Analysis/Function_Topology.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Product_Topology.thy
src/HOL/Analysis/T1_Spaces.thy
src/HOL/Library/FuncSet.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Mar 20 23:06:51 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Mar 21 14:18:22 2019 +0000
     1.3 @@ -1410,7 +1410,10 @@
     1.4    by (simp add: Sup_le_iff closure_of_minimal)
     1.5  
     1.6  
     1.7 -subsection\<open>Continuous maps\<close>
     1.8 +subsection%important \<open>Continuous maps\<close>
     1.9 +
    1.10 +text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
    1.11 +of type classes, as defined below.\<close>
    1.12  
    1.13  definition continuous_map where
    1.14    "continuous_map X Y f \<equiv>
    1.15 @@ -1717,6 +1720,22 @@
    1.16  declare continuous_map_id_subt [unfolded id_def, simp]
    1.17  
    1.18  
    1.19 +lemma%important continuous_map_alt:
    1.20 +   "continuous_map T1 T2 f 
    1.21 +    = ((\<forall>U. openin T2 U \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)) \<and> f ` topspace T1 \<subseteq> topspace T2)"
    1.22 +  by (auto simp: continuous_map_def vimage_def image_def Collect_conj_eq inf_commute)
    1.23 +
    1.24 +lemma continuous_map_open [intro]:
    1.25 +  "continuous_map T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
    1.26 +  unfolding continuous_map_alt by auto
    1.27 +
    1.28 +lemma continuous_map_preimage_topspace [intro]:
    1.29 +  assumes "continuous_map T1 T2 f"
    1.30 +  shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
    1.31 +using assms unfolding continuous_map_def by auto
    1.32 +
    1.33 +
    1.34 +
    1.35  subsection\<open>Open and closed maps (not a priori assumed continuous)\<close>
    1.36  
    1.37  definition open_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
    1.38 @@ -1852,7 +1871,7 @@
    1.39    apply clarify
    1.40    apply (rename_tac T)
    1.41    apply (rule_tac x="f ` T" in image_eqI)
    1.42 -  using openin_closedin_eq by force+
    1.43 +  using openin_closedin_eq by fastforce+
    1.44  
    1.45  lemma closed_map_restriction:
    1.46       "\<lbrakk>closed_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
    1.47 @@ -1861,7 +1880,7 @@
    1.48    apply clarify
    1.49    apply (rename_tac T)
    1.50    apply (rule_tac x="f ` T" in image_eqI)
    1.51 -  using closedin_def by force+
    1.52 +  using closedin_def by fastforce+
    1.53  
    1.54  subsection\<open>Quotient maps\<close>
    1.55                                        
    1.56 @@ -4177,35 +4196,10 @@
    1.57    qed
    1.58  qed
    1.59  
    1.60 -subsubsection%important \<open>Continuity\<close>
    1.61 -
    1.62 -text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
    1.63 -of type classes, as defined below.\<close>
    1.64 -
    1.65 -definition%important continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
    1.66 -  where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
    1.67 -                                      \<and> (f`(topspace T1) \<subseteq> (topspace T2)))"
    1.68 -
    1.69 -lemma continuous_on_continuous_on_topo:
    1.70 -  "continuous_on s f \<longleftrightarrow> continuous_on_topo (top_of_set s) euclidean f"
    1.71 -  by (auto simp: continuous_on_topo_def Int_commute continuous_openin_preimage_eq)
    1.72 -
    1.73 -lemma continuous_on_topo_UNIV:
    1.74 -  "continuous_on UNIV f \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
    1.75 -using continuous_on_continuous_on_topo[of UNIV f] subtopology_UNIV[of euclidean] by auto
    1.76 -
    1.77 -lemma continuous_on_topo_open [intro]:
    1.78 -  "continuous_on_topo T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
    1.79 -  unfolding continuous_on_topo_def by auto
    1.80 -
    1.81 -lemma continuous_on_topo_topspace [intro]:
    1.82 -  "continuous_on_topo T1 T2 f \<Longrightarrow> f`(topspace T1) \<subseteq> (topspace T2)"
    1.83 -unfolding continuous_on_topo_def by auto
    1.84 -
    1.85  lemma continuous_on_generated_topo_iff:
    1.86 -  "continuous_on_topo T1 (topology_generated_by S) f \<longleftrightarrow>
    1.87 +  "continuous_map T1 (topology_generated_by S) f \<longleftrightarrow>
    1.88        ((\<forall>U. U \<in> S \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1))) \<and> (f`(topspace T1) \<subseteq> (\<Union> S)))"
    1.89 -unfolding continuous_on_topo_def topology_generated_by_topspace
    1.90 +unfolding continuous_map_alt topology_generated_by_topspace
    1.91  proof (auto simp add: topology_generated_by_Basis)
    1.92    assume H: "\<forall>U. U \<in> S \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)"
    1.93    fix U assume "openin (topology_generated_by S) U"
    1.94 @@ -4231,31 +4225,11 @@
    1.95  lemma continuous_on_generated_topo:
    1.96    assumes "\<And>U. U \<in>S \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
    1.97            "f`(topspace T1) \<subseteq> (\<Union> S)"
    1.98 -  shows "continuous_on_topo T1 (topology_generated_by S) f"
    1.99 +  shows "continuous_map T1 (topology_generated_by S) f"
   1.100    using assms continuous_on_generated_topo_iff by blast
   1.101  
   1.102 -proposition continuous_on_topo_compose:
   1.103 -  assumes "continuous_on_topo T1 T2 f" "continuous_on_topo T2 T3 g"
   1.104 -  shows "continuous_on_topo T1 T3 (g o f)"
   1.105 -  using assms unfolding continuous_on_topo_def
   1.106 -proof (auto)
   1.107 -  fix U :: "'c set"
   1.108 -  assume H: "openin T3 U"
   1.109 -  have "openin T1 (f -` (g -` U \<inter> topspace T2) \<inter> topspace T1)"
   1.110 -    using H assms by blast
   1.111 -  moreover have "f -` (g -` U \<inter> topspace T2) \<inter> topspace T1 = (g \<circ> f) -` U \<inter> topspace T1"
   1.112 -    using H assms continuous_on_topo_topspace by fastforce
   1.113 -  ultimately show "openin T1 ((g \<circ> f) -` U \<inter> topspace T1)"
   1.114 -    by simp
   1.115 -qed (blast)
   1.116 -
   1.117 -lemma continuous_on_topo_preimage_topspace [intro]:
   1.118 -  assumes "continuous_on_topo T1 T2 f"
   1.119 -  shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
   1.120 -using assms unfolding continuous_on_topo_def by auto
   1.121 -
   1.122 -
   1.123 -subsubsection%important \<open>Pullback topology\<close>
   1.124 +
   1.125 +subsection%important \<open>Pullback topology\<close>
   1.126  
   1.127  text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
   1.128  a special case of this notion, pulling back by the identity. We introduce the general notion as
   1.129 @@ -4289,14 +4263,14 @@
   1.130    "topspace (pullback_topology A f T) = f-`(topspace T) \<inter> A"
   1.131  by (auto simp add: topspace_def openin_pullback_topology)
   1.132  
   1.133 -proposition continuous_on_topo_pullback [intro]:
   1.134 -  assumes "continuous_on_topo T1 T2 g"
   1.135 -  shows "continuous_on_topo (pullback_topology A f T1) T2 (g o f)"
   1.136 -unfolding continuous_on_topo_def
   1.137 +proposition continuous_map_pullback [intro]:
   1.138 +  assumes "continuous_map T1 T2 g"
   1.139 +  shows "continuous_map (pullback_topology A f T1) T2 (g o f)"
   1.140 +unfolding continuous_map_alt
   1.141  proof (auto)
   1.142    fix U::"'b set" assume "openin T2 U"
   1.143    then have "openin T1 (g-`U \<inter> topspace T1)"
   1.144 -    using assms unfolding continuous_on_topo_def by auto
   1.145 +    using assms unfolding continuous_map_alt by auto
   1.146    have "(g o f)-`U \<inter> topspace (pullback_topology A f T1) = (g o f)-`U \<inter> A \<inter> f-`(topspace T1)"
   1.147      unfolding topspace_pullback_topology by auto
   1.148    also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
   1.149 @@ -4310,13 +4284,13 @@
   1.150    then have "f x \<in> topspace T1"
   1.151      unfolding topspace_pullback_topology by auto
   1.152    then show "g (f x) \<in> topspace T2"
   1.153 -    using assms unfolding continuous_on_topo_def by auto
   1.154 +    using assms unfolding continuous_map_def by auto
   1.155  qed
   1.156  
   1.157 -proposition continuous_on_topo_pullback' [intro]:
   1.158 -  assumes "continuous_on_topo T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
   1.159 -  shows "continuous_on_topo T1 (pullback_topology A f T2) g"
   1.160 -unfolding continuous_on_topo_def
   1.161 +proposition continuous_map_pullback' [intro]:
   1.162 +  assumes "continuous_map T1 T2 (f o g)" "topspace T1 \<subseteq> g-`A"
   1.163 +  shows "continuous_map T1 (pullback_topology A f T2) g"
   1.164 +unfolding continuous_map_alt
   1.165  proof (auto)
   1.166    fix U assume "openin (pullback_topology A f T2) U"
   1.167    then have "\<exists>V. openin T2 V \<and> U = f-`V \<inter> A"
   1.168 @@ -4335,7 +4309,7 @@
   1.169  next
   1.170    fix x assume "x \<in> topspace T1"
   1.171    have "(f o g) x \<in> topspace T2"
   1.172 -    using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
   1.173 +    using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
   1.174    then have "g x \<in> f-`(topspace T2)"
   1.175      unfolding comp_def by blast
   1.176    moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
     2.1 --- a/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Mar 20 23:06:51 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Thu Mar 21 14:18:22 2019 +0000
     2.3 @@ -1231,6 +1231,15 @@
     2.4  lemma pathin_const:
     2.5     "pathin X (\<lambda>x. a) \<longleftrightarrow> a \<in> topspace X"
     2.6    by (simp add: pathin_def)
     2.7 +   
     2.8 +lemma path_start_in_topspace: "pathin X g \<Longrightarrow> g 0 \<in> topspace X"
     2.9 +  by (force simp: pathin_def continuous_map)
    2.10 +
    2.11 +lemma path_finish_in_topspace: "pathin X g \<Longrightarrow> g 1 \<in> topspace X"
    2.12 +  by (force simp: pathin_def continuous_map)
    2.13 +
    2.14 +lemma path_image_subset_topspace: "pathin X g \<Longrightarrow> g ` ({0..1}) \<subseteq> topspace X"
    2.15 +  by (force simp: pathin_def continuous_map)
    2.16  
    2.17  definition path_connected_space :: "'a topology \<Rightarrow> bool"
    2.18    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"
    2.19 @@ -1323,6 +1332,19 @@
    2.20    qed
    2.21  qed
    2.22  
    2.23 +lemma path_connectedin_discrete_topology:
    2.24 +  "path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
    2.25 +  apply safe
    2.26 +  using path_connectedin_subset_topspace apply fastforce
    2.27 +   apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
    2.28 +  using subset_singletonD by fastforce
    2.29 +
    2.30 +lemma path_connected_space_discrete_topology:
    2.31 +   "path_connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
    2.32 +  by (metis path_connectedin_discrete_topology path_connectedin_topspace path_connected_space_topspace_empty
    2.33 +            subset_singletonD topspace_discrete_topology)
    2.34 +
    2.35 +
    2.36  lemma homeomorphic_path_connected_space_imp:
    2.37       "\<lbrakk>path_connected_space X; X homeomorphic_space Y\<rbrakk> \<Longrightarrow> path_connected_space Y"
    2.38    unfolding homeomorphic_space_def homeomorphic_maps_def
     3.1 --- a/src/HOL/Analysis/Binary_Product_Measure.thy	Wed Mar 20 23:06:51 2019 +0100
     3.2 +++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Thu Mar 21 14:18:22 2019 +0000
     3.3 @@ -74,11 +74,11 @@
     3.4  qed
     3.5  
     3.6  lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^sub>M M2) M1"
     3.7 -  by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
     3.8 +  by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space Times_Int_Times
     3.9      measurable_def)
    3.10  
    3.11  lemma measurable_snd[intro!, simp, measurable]: "snd \<in> measurable (M1 \<Otimes>\<^sub>M M2) M2"
    3.12 -  by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times
    3.13 +  by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space Times_Int_Times
    3.14      measurable_def)
    3.15  
    3.16  lemma measurable_Pair_compose_split[measurable_dest]:
    3.17 @@ -215,7 +215,7 @@
    3.18  
    3.19  lemma Int_stable_pair_measure_generator: "Int_stable {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}"
    3.20    unfolding Int_stable_def
    3.21 -  by safe (auto simp add: times_Int_times)
    3.22 +  by safe (auto simp add: Times_Int_Times)
    3.23  
    3.24  lemma (in finite_measure) finite_measure_cut_measurable:
    3.25    assumes [measurable]: "Q \<in> sets (N \<Otimes>\<^sub>M M)"
     4.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Mar 20 23:06:51 2019 +0100
     4.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Mar 21 14:18:22 2019 +0000
     4.3 @@ -779,41 +779,41 @@
     4.4  qed
     4.5  
     4.6  lemma strong_operator_topology_continuous_evaluation:
     4.7 -  "continuous_on_topo strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
     4.8 +  "continuous_map strong_operator_topology euclidean (\<lambda>f. blinfun_apply f x)"
     4.9  proof -
    4.10 -  have "continuous_on_topo strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
    4.11 -    unfolding strong_operator_topology_def apply (rule continuous_on_topo_pullback)
    4.12 -    using continuous_on_topo_UNIV continuous_on_product_coordinates by fastforce
    4.13 +  have "continuous_map strong_operator_topology euclidean ((\<lambda>f. f x) o blinfun_apply)"
    4.14 +    unfolding strong_operator_topology_def apply (rule continuous_map_pullback)
    4.15 +    using continuous_on_product_coordinates by fastforce
    4.16    then show ?thesis unfolding comp_def by simp
    4.17  qed
    4.18  
    4.19  lemma continuous_on_strong_operator_topo_iff_coordinatewise:
    4.20 -  "continuous_on_topo T strong_operator_topology f
    4.21 -    \<longleftrightarrow> (\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x))"
    4.22 +  "continuous_map T strong_operator_topology f
    4.23 +    \<longleftrightarrow> (\<forall>x. continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x))"
    4.24  proof (auto)
    4.25    fix x::"'b"
    4.26 -  assume "continuous_on_topo T strong_operator_topology f"
    4.27 -  with continuous_on_topo_compose[OF this strong_operator_topology_continuous_evaluation]
    4.28 -  have "continuous_on_topo T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
    4.29 +  assume "continuous_map T strong_operator_topology f"
    4.30 +  with continuous_map_compose[OF this strong_operator_topology_continuous_evaluation]
    4.31 +  have "continuous_map T euclidean ((\<lambda>z. blinfun_apply z x) o f)"
    4.32      by simp
    4.33 -  then show "continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
    4.34 +  then show "continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x)"
    4.35      unfolding comp_def by auto
    4.36  next
    4.37 -  assume *: "\<forall>x. continuous_on_topo T euclidean (\<lambda>y. blinfun_apply (f y) x)"
    4.38 -  have "continuous_on_topo T euclidean (blinfun_apply o f)"
    4.39 +  assume *: "\<forall>x. continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x)"
    4.40 +  have "continuous_map T euclidean (blinfun_apply o f)"
    4.41      unfolding euclidean_product_topology
    4.42 -    apply (rule continuous_on_topo_coordinatewise_then_product, auto)
    4.43 +    apply (rule continuous_map_coordinatewise_then_product, auto)
    4.44      using * unfolding comp_def by auto
    4.45 -  show "continuous_on_topo T strong_operator_topology f"
    4.46 +  show "continuous_map T strong_operator_topology f"
    4.47      unfolding strong_operator_topology_def
    4.48 -    apply (rule continuous_on_topo_pullback')
    4.49 -    by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
    4.50 +    apply (rule continuous_map_pullback')
    4.51 +    by (auto simp add: \<open>continuous_map T euclidean (blinfun_apply o f)\<close>)
    4.52  qed
    4.53  
    4.54  lemma strong_operator_topology_weaker_than_euclidean:
    4.55 -  "continuous_on_topo euclidean strong_operator_topology (\<lambda>f. f)"
    4.56 +  "continuous_map euclidean strong_operator_topology (\<lambda>f. f)"
    4.57    by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
    4.58 -    auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
    4.59 +    auto simp add: linear_continuous_on)
    4.60  
    4.61  
    4.62  
     5.1 --- a/src/HOL/Analysis/Function_Topology.thy	Wed Mar 20 23:06:51 2019 +0100
     5.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Thu Mar 21 14:18:22 2019 +0000
     5.3 @@ -3,11 +3,11 @@
     5.4  *)
     5.5  
     5.6  theory Function_Topology
     5.7 -imports Topology_Euclidean_Space   
     5.8 +imports Topology_Euclidean_Space
     5.9  begin
    5.10  
    5.11  
    5.12 -section \<open>Function Topology\<close> 
    5.13 +section \<open>Function Topology\<close>
    5.14  
    5.15  text \<open>We want to define the general product topology.
    5.16  
    5.17 @@ -42,17 +42,17 @@
    5.18  
    5.19  Here is an example of a reformulation using topologies. Let
    5.20  @{text [display]
    5.21 -\<open>continuous_on_topo T1 T2 f =
    5.22 +\<open>continuous_map T1 T2 f =
    5.23      ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
    5.24              \<and> (f`(topspace T1) \<subseteq> (topspace T2)))\<close>}
    5.25  be the natural continuity definition of a map from the topology \<open>T1\<close> to the topology \<open>T2\<close>. Then
    5.26  the current \<open>continuous_on\<close> (with type classes) can be redefined as
    5.27  @{text [display] \<open>continuous_on s f =
    5.28 -    continuous_on_topo (top_of_set s) (topology euclidean) f\<close>}
    5.29 +    continuous_map (top_of_set s) (topology euclidean) f\<close>}
    5.30  
    5.31 -In fact, I need \<open>continuous_on_topo\<close> to express the continuity of the projection on subfactors
    5.32 +In fact, I need \<open>continuous_map\<close> to express the continuity of the projection on subfactors
    5.33  for the product topology, in Lemma~\<open>continuous_on_restrict_product_topology\<close>, and I show
    5.34 -the above equivalence in Lemma~\<open>continuous_on_continuous_on_topo\<close>.
    5.35 +the above equivalence in Lemma~\<open>continuous_map_iff_continuous\<close>.
    5.36  
    5.37  I only develop the basics of the product topology in this theory. The most important missing piece
    5.38  is Tychonov theorem, stating that a product of compact spaces is always compact for the product
    5.39 @@ -252,7 +252,7 @@
    5.40            ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
    5.41             relative_to topspace (product_topology X I))"
    5.42    apply (subst product_topology)
    5.43 -  apply (simp add: topspace_product_topology topology_inverse' [OF istopology_subbase])
    5.44 +  apply (simp add: topology_inverse' [OF istopology_subbase])
    5.45    done
    5.46  
    5.47  lemma subtopology_PiE:
    5.48 @@ -286,10 +286,9 @@
    5.49    done
    5.50  qed
    5.51  
    5.52 -
    5.53  lemma product_topology_base_alt:
    5.54     "finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
    5.55 -    relative_to topspace(product_topology X I) =
    5.56 +    relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i)) =
    5.57      (\<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))))"
    5.58     (is "?lhs = ?rhs")
    5.59  proof -
    5.60 @@ -340,6 +339,15 @@
    5.61      by meson
    5.62  qed
    5.63  
    5.64 +corollary openin_product_topology_alt:
    5.65 +  "openin (product_topology X I) S \<longleftrightarrow>
    5.66 +    (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
    5.67 +                 (\<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)"
    5.68 +  unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology
    5.69 +  apply safe
    5.70 +  apply (drule bspec; blast)+
    5.71 +  done
    5.72 +
    5.73  lemma closure_of_product_topology:
    5.74    "(product_topology X I) closure_of (PiE I S) = PiE I (\<lambda>i. (X i) closure_of (S i))"
    5.75  proof -
    5.76 @@ -445,9 +453,9 @@
    5.77  
    5.78  subsubsection \<open>The basic property of the product topology is the continuity of projections:\<close>
    5.79  
    5.80 -lemma continuous_on_topo_product_coordinates [simp]:
    5.81 +lemma continuous_map_product_coordinates [simp]:
    5.82    assumes "i \<in> I"
    5.83 -  shows "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. x i)"
    5.84 +  shows "continuous_map (product_topology T I) (T i) (\<lambda>x. x i)"
    5.85  proof -
    5.86    {
    5.87      fix U assume "openin (T i) U"
    5.88 @@ -463,14 +471,14 @@
    5.89        apply (subst *)
    5.90        using ** by auto
    5.91    }
    5.92 -  then show ?thesis unfolding continuous_on_topo_def
    5.93 -    by (auto simp add: assms topspace_product_topology PiE_iff)
    5.94 +  then show ?thesis unfolding continuous_map_alt
    5.95 +    by (auto simp add: assms PiE_iff)
    5.96  qed
    5.97  
    5.98 -lemma continuous_on_topo_coordinatewise_then_product [intro]:
    5.99 -  assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
   5.100 +lemma continuous_map_coordinatewise_then_product [intro]:
   5.101 +  assumes "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
   5.102            "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
   5.103 -  shows "continuous_on_topo T1 (product_topology T I) f"
   5.104 +  shows "continuous_map T1 (product_topology T I) f"
   5.105  unfolding product_topology_def
   5.106  proof (rule continuous_on_generated_topo)
   5.107    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)}}"
   5.108 @@ -479,7 +487,7 @@
   5.109    define J where "J = {i \<in> I. X i \<noteq> topspace (T i)}"
   5.110    have "finite J" "J \<subseteq> I" unfolding J_def using H(3) by auto
   5.111    have "(\<lambda>x. f x i)-`(topspace(T i)) \<inter> topspace T1 = topspace T1" if "i \<in> I" for i
   5.112 -    using that assms(1) by (simp add: continuous_on_topo_preimage_topspace)
   5.113 +    using that assms(1) by (simp add: continuous_map_preimage_topspace)
   5.114    then have *: "(\<lambda>x. f x i)-`(X i) \<inter> topspace T1 = topspace T1" if "i \<in> I-J" for i
   5.115      using that unfolding J_def by auto
   5.116    have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
   5.117 @@ -497,25 +505,25 @@
   5.118      apply (subst product_topology_def[symmetric])
   5.119      apply (simp only: topspace_product_topology)
   5.120      apply (auto simp add: PiE_iff)
   5.121 -    using assms unfolding continuous_on_topo_def by auto
   5.122 +    using assms unfolding continuous_map_def by auto
   5.123  qed
   5.124  
   5.125 -lemma continuous_on_topo_product_then_coordinatewise [intro]:
   5.126 -  assumes "continuous_on_topo T1 (product_topology T I) f"
   5.127 -  shows "\<And>i. i \<in> I \<Longrightarrow> continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
   5.128 +lemma continuous_map_product_then_coordinatewise [intro]:
   5.129 +  assumes "continuous_map T1 (product_topology T I) f"
   5.130 +  shows "\<And>i. i \<in> I \<Longrightarrow> continuous_map T1 (T i) (\<lambda>x. f x i)"
   5.131          "\<And>i x. i \<notin> I \<Longrightarrow> x \<in> topspace T1 \<Longrightarrow> f x i = undefined"
   5.132  proof -
   5.133    fix i assume "i \<in> I"
   5.134    have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
   5.135 -  also have "continuous_on_topo T1 (T i) (...)"
   5.136 -    apply (rule continuous_on_topo_compose[of _ "product_topology T I"])
   5.137 +  also have "continuous_map T1 (T i) (...)"
   5.138 +    apply (rule continuous_map_compose[of _ "product_topology T I"])
   5.139      using assms \<open>i \<in> I\<close> by auto
   5.140 -  ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
   5.141 +  ultimately show "continuous_map T1 (T i) (\<lambda>x. f x i)"
   5.142      by simp
   5.143  next
   5.144    fix i x assume "i \<notin> I" "x \<in> topspace T1"
   5.145    have "f x \<in> topspace (product_topology T I)"
   5.146 -    using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
   5.147 +    using assms \<open>x \<in> topspace T1\<close> unfolding continuous_map_def by auto
   5.148    then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
   5.149      using topspace_product_topology by metis
   5.150    then show "f x i = undefined"
   5.151 @@ -524,11 +532,11 @@
   5.152  
   5.153  lemma continuous_on_restrict:
   5.154    assumes "J \<subseteq> I"
   5.155 -  shows "continuous_on_topo (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
   5.156 -proof (rule continuous_on_topo_coordinatewise_then_product)
   5.157 +  shows "continuous_map (product_topology T I) (product_topology T J) (\<lambda>x. restrict x J)"
   5.158 +proof (rule continuous_map_coordinatewise_then_product)
   5.159    fix i assume "i \<in> J"
   5.160    then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
   5.161 -  then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
   5.162 +  then show "continuous_map (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
   5.163      using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
   5.164  next
   5.165    fix i assume "i \<notin> J"
   5.166 @@ -571,7 +579,7 @@
   5.167    have **: "finite {i. X i \<noteq> UNIV}"
   5.168      unfolding X_def V_def J_def using assms(1) by auto
   5.169    have "open (Pi\<^sub>E UNIV X)"
   5.170 -    unfolding open_fun_def 
   5.171 +    unfolding open_fun_def
   5.172      by (simp_all add: * ** product_topology_basis)
   5.173    moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
   5.174      apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
   5.175 @@ -594,28 +602,28 @@
   5.176  
   5.177  lemma continuous_on_product_coordinates [simp]:
   5.178    "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
   5.179 -  unfolding continuous_on_topo_UNIV euclidean_product_topology
   5.180 -  by (rule continuous_on_topo_product_coordinates, simp)
   5.181 +  using continuous_map_product_coordinates [of _ UNIV "\<lambda>i. euclidean"]
   5.182 +    by (metis (no_types) continuous_map_iff_continuous euclidean_product_topology iso_tuple_UNIV_I subtopology_UNIV)
   5.183  
   5.184  lemma continuous_on_coordinatewise_then_product [intro, continuous_intros]:
   5.185    fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
   5.186    assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
   5.187    shows "continuous_on S f"
   5.188 -  using continuous_on_topo_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
   5.189 -  by (metis UNIV_I assms continuous_on_continuous_on_topo euclidean_product_topology)
   5.190 +  using continuous_map_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
   5.191 +  by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology)
   5.192  
   5.193  lemma continuous_on_product_then_coordinatewise_UNIV:
   5.194    assumes "continuous_on UNIV f"
   5.195    shows "continuous_on UNIV (\<lambda>x. f x i)"
   5.196 -using assms unfolding continuous_on_topo_UNIV euclidean_product_topology
   5.197 -by (rule continuous_on_topo_product_then_coordinatewise(1), simp)
   5.198 +  using assms unfolding continuous_map_iff_continuous2 [symmetric] euclidean_product_topology
   5.199 +  by fastforce
   5.200  
   5.201  lemma continuous_on_product_then_coordinatewise:
   5.202    assumes "continuous_on S f"
   5.203    shows "continuous_on S (\<lambda>x. f x i)"
   5.204  proof -
   5.205    have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
   5.206 -    by (metis assms continuous_on_compose continuous_on_id 
   5.207 +    by (metis assms continuous_on_compose continuous_on_id
   5.208          continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
   5.209    then show ?thesis
   5.210      by auto
   5.211 @@ -1582,4 +1590,166 @@
   5.212    qed
   5.213  qed
   5.214  
   5.215 +subsection \<open>Open Pi-sets in the product topology\<close>
   5.216 +
   5.217 +proposition openin_PiE_gen:
   5.218 +  "openin (product_topology X I) (PiE I S) \<longleftrightarrow>
   5.219 +        PiE I S = {} \<or>
   5.220 +        finite {i \<in> I. ~(S i = topspace(X i))} \<and> (\<forall>i \<in> I. openin (X i) (S i))"
   5.221 +  (is "?lhs \<longleftrightarrow> _ \<or> ?rhs")
   5.222 +proof (cases "PiE I S = {}")
   5.223 +  case False
   5.224 +  moreover have "?lhs = ?rhs"
   5.225 +  proof
   5.226 +    assume L: ?lhs
   5.227 +    moreover
   5.228 +    obtain z where z: "z \<in> PiE I S"
   5.229 +      using False by blast
   5.230 +    ultimately obtain U where fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
   5.231 +      and "Pi\<^sub>E I U \<noteq> {}"
   5.232 +      and sub: "Pi\<^sub>E I U \<subseteq> Pi\<^sub>E I S"
   5.233 +      by (fastforce simp add: openin_product_topology_alt)
   5.234 +    then have *: "\<And>i. i \<in> I \<Longrightarrow> U i \<subseteq> S i"
   5.235 +      by (simp add: subset_PiE)
   5.236 +    show ?rhs
   5.237 +    proof (intro conjI ballI)
   5.238 +      show "finite {i \<in> I. S i \<noteq> topspace (X i)}"
   5.239 +        apply (rule finite_subset [OF _ fin], clarify)
   5.240 +        using *
   5.241 +        by (metis False L openin_subset topspace_product_topology subset_PiE subset_antisym)
   5.242 +    next
   5.243 +      fix i :: "'a"
   5.244 +      assume "i \<in> I"
   5.245 +      then show "openin (X i) (S i)"
   5.246 +        using open_map_product_projection [of i I X] L
   5.247 +        apply (simp add: open_map_def)
   5.248 +        apply (drule_tac x="PiE I S" in spec)
   5.249 +        apply (simp add: False image_projection_PiE split: if_split_asm)
   5.250 +        done
   5.251 +    qed
   5.252 +  next
   5.253 +    assume ?rhs
   5.254 +    then show ?lhs
   5.255 +      apply (simp only: openin_product_topology)
   5.256 +      apply (rule arbitrary_union_of_inc)
   5.257 +      apply (auto simp: product_topology_base_alt)
   5.258 +      done
   5.259 +  qed
   5.260 +  ultimately show ?thesis
   5.261 +    by simp
   5.262 +qed simp
   5.263 +
   5.264 +
   5.265 +corollary openin_PiE:
   5.266 +   "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))"
   5.267 +  by (simp add: openin_PiE_gen)
   5.268 +
   5.269 +proposition compact_space_product_topology:
   5.270 +   "compact_space(product_topology X I) \<longleftrightarrow>
   5.271 +    topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. compact_space(X i))"
   5.272 +    (is "?lhs = ?rhs")
   5.273 +proof (cases "topspace(product_topology X I) = {}")
   5.274 +  case False
   5.275 +  then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
   5.276 +    by auto
   5.277 +  show ?thesis
   5.278 +  proof
   5.279 +    assume L: ?lhs
   5.280 +    show ?rhs
   5.281 +    proof (clarsimp simp add: False compact_space_def)
   5.282 +      fix i
   5.283 +      assume "i \<in> I"
   5.284 +      with L have "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
   5.285 +        by (simp add: continuous_map_product_projection)
   5.286 +      moreover
   5.287 +      have "\<And>x. x \<in> topspace (X i) \<Longrightarrow> x \<in> (\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
   5.288 +        using \<open>i \<in> I\<close> z
   5.289 +        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)
   5.290 +        done
   5.291 +      then have "(\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = topspace (X i)"
   5.292 +        using \<open>i \<in> I\<close> z by auto
   5.293 +      ultimately show "compactin (X i) (topspace (X i))"
   5.294 +        by (metis L compact_space_def image_compactin topspace_product_topology)
   5.295 +    qed
   5.296 +  next
   5.297 +    assume R: ?rhs
   5.298 +    show ?lhs
   5.299 +    proof (cases "I = {}")
   5.300 +      case True
   5.301 +      with R show ?thesis
   5.302 +        by (simp add: compact_space_def)
   5.303 +    next
   5.304 +      case False
   5.305 +      then obtain i where "i \<in> I"
   5.306 +        by blast
   5.307 +      show ?thesis
   5.308 +        using R
   5.309 +      proof
   5.310 +        assume com [rule_format]: "\<forall>i\<in>I. compact_space (X i)"
   5.311 +        let ?\<C> = "{{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
   5.312 +        show "compact_space (product_topology X I)"
   5.313 +        proof (rule Alexander_subbase_alt)
   5.314 +          show "topspace (product_topology X I) \<subseteq> \<Union>?\<C>"
   5.315 +            unfolding topspace_product_topology using \<open>i \<in> I\<close> by blast
   5.316 +        next
   5.317 +          fix C
   5.318 +          assume Csub: "C \<subseteq> ?\<C>" and UC: "topspace (product_topology X I) \<subseteq> \<Union>C"
   5.319 +          define \<D> where "\<D> \<equiv> \<lambda>i. {U. openin (X i) U \<and> {f. f i \<in> U} \<in> C}"
   5.320 +          show "\<exists>C'. finite C' \<and> C' \<subseteq> C \<and> topspace (product_topology X I) \<subseteq> \<Union>C'"
   5.321 +          proof (cases "\<exists>i. i \<in> I \<and> topspace (X i) \<subseteq> \<Union>(\<D> i)")
   5.322 +            case True
   5.323 +            then obtain i where "i \<in> I"
   5.324 +                   and i: "topspace (X i) \<subseteq> \<Union>(\<D> i)"
   5.325 +              unfolding \<D>_def by blast
   5.326 +            then have *: "\<And>\<U>. \<lbrakk>Ball \<U> (openin (X i)); topspace (X i) \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow>
   5.327 +                            \<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace (X i) \<subseteq> \<Union>\<F>"
   5.328 +              using com [OF \<open>i \<in> I\<close>] by (auto simp: compact_space_def compactin_def)
   5.329 +            have "topspace (X i) \<subseteq> \<Union>(\<D> i)"
   5.330 +              using i by auto
   5.331 +            with * obtain \<F> where "finite \<F> \<and> \<F> \<subseteq> (\<D> i) \<and> topspace (X i) \<subseteq> \<Union>\<F>"
   5.332 +              unfolding \<D>_def by fastforce
   5.333 +            with \<open>i \<in> I\<close> show ?thesis
   5.334 +              unfolding \<D>_def
   5.335 +              by (rule_tac x="(\<lambda>U. {x. x i \<in> U}) ` \<F>" in exI) auto
   5.336 +          next
   5.337 +            case False
   5.338 +            then have "\<forall>i \<in> I. \<exists>y. y \<in> topspace (X i) \<and> y \<notin> \<Union>(\<D> i)"
   5.339 +              by force
   5.340 +            then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> g i \<in> topspace (X i) \<and> g i \<notin> \<Union>(\<D> i)"
   5.341 +              by metis
   5.342 +            then have "(\<lambda>i. if i \<in> I then g i else undefined) \<in> topspace (product_topology X I)"
   5.343 +              by (simp add: PiE_I)
   5.344 +            moreover have "(\<lambda>i. if i \<in> I then g i else undefined) \<notin> \<Union>C"
   5.345 +              using Csub g unfolding \<D>_def by force
   5.346 +            ultimately show ?thesis
   5.347 +              using UC by blast
   5.348 +          qed
   5.349 +        qed (simp add: product_topology)
   5.350 +      qed (simp add: compact_space_topspace_empty)
   5.351 +    qed
   5.352 +  qed
   5.353 +qed (simp add: compact_space_topspace_empty)
   5.354 +
   5.355 +corollary compactin_PiE:
   5.356 +   "compactin (product_topology X I) (PiE I S) \<longleftrightarrow>
   5.357 +        PiE I S = {} \<or> (\<forall>i \<in> I. compactin (X i) (S i))"
   5.358 +  by (auto simp: compactin_subspace subtopology_PiE subset_PiE compact_space_product_topology
   5.359 +       PiE_eq_empty_iff)
   5.360 +
   5.361 +lemma in_product_topology_closure_of:
   5.362 +   "z \<in> (product_topology X I) closure_of S
   5.363 +        \<Longrightarrow> i \<in> I \<Longrightarrow> z i \<in> ((X i) closure_of ((\<lambda>x. x i) ` S))"
   5.364 +  using continuous_map_product_projection
   5.365 +  by (force simp: continuous_map_eq_image_closure_subset image_subset_iff)
   5.366 +
   5.367 +lemma homeomorphic_space_singleton_product:
   5.368 +   "product_topology X {k} homeomorphic_space (X k)"
   5.369 +  unfolding homeomorphic_space
   5.370 +  apply (rule_tac x="\<lambda>x. x k" in exI)
   5.371 +  apply (rule bijective_open_imp_homeomorphic_map)
   5.372 +     apply (simp_all add: continuous_map_product_projection open_map_product_projection)
   5.373 +  unfolding PiE_over_singleton_iff
   5.374 +   apply (auto simp: image_iff inj_on_def)
   5.375 +  done
   5.376 +
   5.377  end
     6.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed Mar 20 23:06:51 2019 +0100
     6.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Mar 21 14:18:22 2019 +0000
     6.3 @@ -1,4 +1,4 @@
     6.4 -subsection \<open>Ordered Euclidean Space\<close> (* why not Section? *)
     6.5 +section \<open>Ordered Euclidean Space\<close>
     6.6  
     6.7  theory Ordered_Euclidean_Space
     6.8  imports
     7.1 --- a/src/HOL/Analysis/Path_Connected.thy	Wed Mar 20 23:06:51 2019 +0100
     7.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Thu Mar 21 14:18:22 2019 +0000
     7.3 @@ -135,6 +135,9 @@
     7.4  
     7.5  subsection%unimportant\<open>Basic lemmas about paths\<close>
     7.6  
     7.7 +lemma pathin_iff_path_real [simp]: "pathin euclideanreal g \<longleftrightarrow> path g"
     7.8 +  by (simp add: pathin_def path_def)
     7.9 +
    7.10  lemma continuous_on_path: "path f \<Longrightarrow> t \<subseteq> {0..1} \<Longrightarrow> continuous_on t f"
    7.11    using continuous_on_subset path_def by blast
    7.12  
    7.13 @@ -1468,7 +1471,7 @@
    7.14  lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y"
    7.15    unfolding path_component_def by auto
    7.16  
    7.17 -lemma path_connected_linepath:
    7.18 +lemma path_component_linepath:
    7.19      fixes s :: "'a::real_normed_vector set"
    7.20      shows "closed_segment a b \<subseteq> s \<Longrightarrow> path_component s a b"
    7.21    unfolding path_component_def
    7.22 @@ -1502,6 +1505,10 @@
    7.23  definition%important "path_connected s \<longleftrightarrow>
    7.24    (\<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)"
    7.25  
    7.26 +lemma path_connectedin_iff_path_connected_real [simp]:
    7.27 +     "path_connectedin euclideanreal S \<longleftrightarrow> path_connected S"
    7.28 +  by (simp add: path_connectedin path_connected_def path_defs)
    7.29 +
    7.30  lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
    7.31    unfolding path_connected_def path_component_def by auto
    7.32  
    7.33 @@ -1818,6 +1825,29 @@
    7.34  lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
    7.35    by (simp add: convex_imp_path_connected is_interval_convex)
    7.36  
    7.37 +lemma path_connectedin_path_image:
    7.38 +  assumes "pathin X g" shows "path_connectedin X (g ` ({0..1}))"
    7.39 +  unfolding pathin_def
    7.40 +proof (rule path_connectedin_continuous_map_image)
    7.41 +  show "continuous_map (subtopology euclideanreal {0..1}) X g"
    7.42 +    using assms pathin_def by blast
    7.43 +qed (auto simp: is_interval_1 is_interval_path_connected)
    7.44 +
    7.45 +lemma path_connected_space_subconnected:
    7.46 +     "path_connected_space X \<longleftrightarrow>
    7.47 +      (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. \<exists>S. path_connectedin X S \<and> x \<in> S \<and> y \<in> S)"
    7.48 +  unfolding path_connected_space_def Ball_def
    7.49 +  apply (intro all_cong1 imp_cong refl, safe)
    7.50 +  using path_connectedin_path_image apply fastforce
    7.51 +  by (meson path_connectedin)
    7.52 +
    7.53 +lemma connectedin_path_image: "pathin X g \<Longrightarrow> connectedin X (g ` ({0..1}))"
    7.54 +  by (simp add: path_connectedin_imp_connectedin path_connectedin_path_image)
    7.55 +
    7.56 +lemma compactin_path_image: "pathin X g \<Longrightarrow> compactin X (g ` ({0..1}))"
    7.57 +  unfolding pathin_def
    7.58 +  by (rule image_compactin [of "top_of_set {0..1}"]) auto
    7.59 +
    7.60  lemma linear_homeomorphism_image:
    7.61    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    7.62    assumes "linear f" "inj f"
    7.63 @@ -1935,6 +1965,372 @@
    7.64  qed
    7.65  
    7.66  
    7.67 +subsection\<open>Path components\<close>
    7.68 +
    7.69 +definition path_component_of
    7.70 +  where "path_component_of X x y \<equiv> \<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y"
    7.71 +
    7.72 +abbreviation path_component_of_set
    7.73 +  where "path_component_of_set X x \<equiv> Collect (path_component_of X x)"
    7.74 +
    7.75 +definition path_components_of :: "'a topology \<Rightarrow> 'a set set"
    7.76 +  where "path_components_of X \<equiv> path_component_of_set X ` topspace X"
    7.77 +
    7.78 +lemma path_component_in_topspace:
    7.79 +   "path_component_of X x y \<Longrightarrow> x \<in> topspace X \<and> y \<in> topspace X"
    7.80 +  by (auto simp: path_component_of_def pathin_def continuous_map_def)
    7.81 +
    7.82 +lemma path_component_of_refl:
    7.83 +   "path_component_of X x x \<longleftrightarrow> x \<in> topspace X"
    7.84 +  apply (auto simp: path_component_in_topspace)
    7.85 +  apply (force simp: path_component_of_def pathin_const)
    7.86 +  done
    7.87 +
    7.88 +lemma path_component_of_sym:
    7.89 +  assumes "path_component_of X x y"
    7.90 +  shows "path_component_of X y x"
    7.91 +  using assms
    7.92 +  apply (clarsimp simp: path_component_of_def pathin_def)
    7.93 +  apply (rule_tac x="g \<circ> (\<lambda>t. 1 - t)" in exI)
    7.94 +  apply (auto intro!: continuous_map_compose)
    7.95 +  apply (force simp: continuous_map_in_subtopology continuous_on_op_minus)
    7.96 +  done
    7.97 +
    7.98 +lemma path_component_of_sym_iff:
    7.99 +   "path_component_of X x y \<longleftrightarrow> path_component_of X y x"
   7.100 +  by (metis path_component_of_sym)
   7.101 +
   7.102 +lemma path_component_of_trans:
   7.103 +  assumes "path_component_of X x y" and "path_component_of X y z"
   7.104 +  shows "path_component_of X x z"
   7.105 +  unfolding path_component_of_def pathin_def
   7.106 +proof -
   7.107 +  let ?T01 = "top_of_set {0..1::real}"
   7.108 +  obtain g1 g2 where g1: "continuous_map ?T01 X g1" "x = g1 0" "y = g1 1"
   7.109 +    and g2: "continuous_map ?T01 X g2" "g2 0 = g1 1" "z = g2 1"
   7.110 +    using assms unfolding path_component_of_def pathin_def by blast
   7.111 +  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"
   7.112 +  show "\<exists>g. continuous_map ?T01 X g \<and> g 0 = x \<and> g 1 = z"
   7.113 +  proof (intro exI conjI)
   7.114 +    show "continuous_map (subtopology euclideanreal {0..1}) X ?g"
   7.115 +    proof (intro continuous_map_cases_le continuous_map_compose, force, force)
   7.116 +      show "continuous_map (subtopology ?T01 {x \<in> topspace ?T01. x \<le> 1/2}) ?T01 ((*) 2)"
   7.117 +        by (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology)
   7.118 +      have "continuous_map
   7.119 +             (subtopology (top_of_set {0..1}) {x. 0 \<le> x \<and> x \<le> 1 \<and> 1 \<le> x * 2})
   7.120 +             euclideanreal (\<lambda>t. 2 * t - 1)"
   7.121 +        by (intro continuous_intros) (force intro: continuous_map_from_subtopology)
   7.122 +      then show "continuous_map (subtopology ?T01 {x \<in> topspace ?T01. 1/2 \<le> x}) ?T01 (\<lambda>t. 2 * t - 1)"
   7.123 +        by (force simp: continuous_map_in_subtopology)
   7.124 +      show "(g1 \<circ> (*) 2) x = (g2 \<circ> (\<lambda>t. 2 * t - 1)) x" if "x \<in> topspace ?T01" "x = 1/2" for x
   7.125 +        using that by (simp add: g2(2) mult.commute continuous_map_from_subtopology)
   7.126 +    qed (auto simp: g1 g2)
   7.127 +  qed (auto simp: g1 g2)
   7.128 +qed
   7.129 +
   7.130 +
   7.131 +lemma path_component_of_mono:
   7.132 +   "\<lbrakk>path_component_of (subtopology X S) x y; S \<subseteq> T\<rbrakk> \<Longrightarrow> path_component_of (subtopology X T) x y"
   7.133 +  unfolding path_component_of_def
   7.134 +  by (metis subsetD pathin_subtopology)
   7.135 +
   7.136 +
   7.137 +lemma path_component_of:
   7.138 +  "path_component_of X x y \<longleftrightarrow> (\<exists>T. path_connectedin X T \<and> x \<in> T \<and> y \<in> T)"
   7.139 +  apply (auto simp: path_component_of_def)
   7.140 +  using path_connectedin_path_image apply fastforce
   7.141 +  apply (metis path_connectedin)
   7.142 +  done
   7.143 +
   7.144 +lemma path_component_of_set:
   7.145 +   "path_component_of X x y \<longleftrightarrow> (\<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y)"
   7.146 +  by (auto simp: path_component_of_def)
   7.147 +
   7.148 +lemma path_component_of_subset_topspace:
   7.149 +   "Collect(path_component_of X x) \<subseteq> topspace X"
   7.150 +  using path_component_in_topspace by fastforce
   7.151 +
   7.152 +lemma path_component_of_eq_empty:
   7.153 +   "Collect(path_component_of X x) = {} \<longleftrightarrow> (x \<notin> topspace X)"
   7.154 +  using path_component_in_topspace path_component_of_refl by fastforce
   7.155 +
   7.156 +lemma path_connected_space_iff_path_component:
   7.157 +   "path_connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. path_component_of X x y)"
   7.158 +  by (simp add: path_component_of path_connected_space_subconnected)
   7.159 +
   7.160 +lemma path_connected_space_imp_path_component_of:
   7.161 +   "\<lbrakk>path_connected_space X; a \<in> topspace X; b \<in> topspace X\<rbrakk>
   7.162 +        \<Longrightarrow> path_component_of X a b"
   7.163 +  by (simp add: path_connected_space_iff_path_component)
   7.164 +
   7.165 +lemma path_connected_space_path_component_set:
   7.166 +   "path_connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. Collect(path_component_of X x) = topspace X)"
   7.167 +  using path_component_of_subset_topspace path_connected_space_iff_path_component by fastforce
   7.168 +
   7.169 +lemma path_component_of_maximal:
   7.170 +   "\<lbrakk>path_connectedin X s; x \<in> s\<rbrakk> \<Longrightarrow> s \<subseteq> Collect(path_component_of X x)"
   7.171 +  using path_component_of by fastforce
   7.172 +
   7.173 +lemma path_component_of_equiv:
   7.174 +   "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"
   7.175 +    (is "?lhs = ?rhs")
   7.176 +proof
   7.177 +  assume ?lhs
   7.178 +  then show ?rhs
   7.179 +    apply (simp add: fun_eq_iff path_component_in_topspace)
   7.180 +    apply (meson path_component_of_sym path_component_of_trans)
   7.181 +    done
   7.182 +qed (simp add: path_component_of_refl)
   7.183 +
   7.184 +lemma path_component_of_disjoint:
   7.185 +     "disjnt (Collect (path_component_of X x)) (Collect (path_component_of X y)) \<longleftrightarrow>
   7.186 +      ~(path_component_of X x y)"
   7.187 +  by (force simp: disjnt_def path_component_of_eq_empty path_component_of_equiv)
   7.188 +
   7.189 +lemma path_component_of_eq:
   7.190 +   "path_component_of X x = path_component_of X y \<longleftrightarrow>
   7.191 +        (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
   7.192 +        x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x y"
   7.193 +  by (metis Collect_empty_eq_bot path_component_of_eq_empty path_component_of_equiv)
   7.194 +
   7.195 +lemma path_connectedin_path_component_of:
   7.196 +  "path_connectedin X (Collect (path_component_of X x))"
   7.197 +proof -
   7.198 +  have "\<And>y. path_component_of X x y
   7.199 +        \<Longrightarrow> path_component_of (subtopology X (Collect (path_component_of X x))) x y"
   7.200 +    by (meson path_component_of path_component_of_maximal path_connectedin_subtopology)
   7.201 +  then show ?thesis
   7.202 +    apply (simp add: path_connectedin_def path_component_of_subset_topspace path_connected_space_iff_path_component)
   7.203 +    by (metis Int_absorb1 mem_Collect_eq path_component_of_equiv path_component_of_subset_topspace topspace_subtopology)
   7.204 +qed
   7.205 +
   7.206 +lemma Union_path_components_of:
   7.207 +     "\<Union>(path_components_of X) = topspace X"
   7.208 +  by (auto simp: path_components_of_def path_component_of_equiv)
   7.209 +
   7.210 +lemma path_components_of_maximal:
   7.211 +   "\<lbrakk>C \<in> path_components_of X; path_connectedin X S; ~disjnt C S\<rbrakk> \<Longrightarrow> S \<subseteq> C"
   7.212 +  apply (auto simp: path_components_of_def path_component_of_equiv)
   7.213 +  using path_component_of_maximal path_connectedin_def apply fastforce
   7.214 +  by (meson disjnt_subset2 path_component_of_disjoint path_component_of_equiv path_component_of_maximal)
   7.215 +
   7.216 +lemma pairwise_disjoint_path_components_of:
   7.217 +     "pairwise disjnt (path_components_of X)"
   7.218 +  by (auto simp: path_components_of_def pairwise_def path_component_of_disjoint path_component_of_equiv)
   7.219 +
   7.220 +lemma complement_path_components_of_Union:
   7.221 +   "C \<in> path_components_of X
   7.222 +        \<Longrightarrow> topspace X - C = \<Union>(path_components_of X - {C})"
   7.223 +  by (metis Diff_cancel Diff_subset Union_path_components_of cSup_singleton diff_Union_pairwise_disjoint insert_subset pairwise_disjoint_path_components_of)
   7.224 +
   7.225 +lemma nonempty_path_components_of:
   7.226 +  "C \<in> path_components_of X \<Longrightarrow> (C \<noteq> {})"
   7.227 +  apply (clarsimp simp: path_components_of_def path_component_of_eq_empty)
   7.228 +  by (meson path_component_of_refl)
   7.229 +
   7.230 +lemma path_components_of_subset: "C \<in> path_components_of X \<Longrightarrow> C \<subseteq> topspace X"
   7.231 +  by (auto simp: path_components_of_def path_component_of_equiv)
   7.232 +
   7.233 +lemma path_connectedin_path_components_of:
   7.234 +   "C \<in> path_components_of X \<Longrightarrow> path_connectedin X C"
   7.235 +  by (auto simp: path_components_of_def path_connectedin_path_component_of)
   7.236 +
   7.237 +lemma path_component_in_path_components_of:
   7.238 +  "Collect (path_component_of X a) \<in> path_components_of X \<longleftrightarrow> a \<in> topspace X"
   7.239 +  apply (rule iffI)
   7.240 +  using nonempty_path_components_of path_component_of_eq_empty apply fastforce
   7.241 +  by (simp add: path_components_of_def)
   7.242 +
   7.243 +lemma path_connectedin_Union:
   7.244 +  assumes \<A>: "\<And>S. S \<in> \<A> \<Longrightarrow> path_connectedin X S" "\<Inter>\<A> \<noteq> {}"
   7.245 +  shows "path_connectedin X (\<Union>\<A>)"
   7.246 +proof -
   7.247 +  obtain a where "\<And>S. S \<in> \<A> \<Longrightarrow> a \<in> S"
   7.248 +    using assms by blast
   7.249 +  then have "\<And>x. x \<in> topspace (subtopology X (\<Union>\<A>)) \<Longrightarrow> path_component_of (subtopology X (\<Union>\<A>)) a x"
   7.250 +    apply (simp add: topspace_subtopology)
   7.251 +    by (meson Union_upper \<A> path_component_of path_connectedin_subtopology)
   7.252 +  then show ?thesis
   7.253 +    using \<A> unfolding path_connectedin_def
   7.254 +    by (metis Sup_le_iff path_component_of_equiv path_connected_space_iff_path_component)
   7.255 +qed
   7.256 +
   7.257 +lemma path_connectedin_Un:
   7.258 +   "\<lbrakk>path_connectedin X S; path_connectedin X T; S \<inter> T \<noteq> {}\<rbrakk>
   7.259 +    \<Longrightarrow> path_connectedin X (S \<union> T)"
   7.260 +  by (blast intro: path_connectedin_Union [of "{S,T}", simplified])
   7.261 +
   7.262 +lemma path_connected_space_iff_components_eq:
   7.263 +  "path_connected_space X \<longleftrightarrow>
   7.264 +    (\<forall>C \<in> path_components_of X. \<forall>C' \<in> path_components_of X. C = C')"
   7.265 +  unfolding path_components_of_def
   7.266 +proof (intro iffI ballI)
   7.267 +  assume "\<forall>C \<in> path_component_of_set X ` topspace X.
   7.268 +             \<forall>C' \<in> path_component_of_set X ` topspace X. C = C'"
   7.269 +  then show "path_connected_space X"
   7.270 +    using path_component_of_refl path_connected_space_iff_path_component by fastforce
   7.271 +qed (auto simp: path_connected_space_path_component_set)
   7.272 +
   7.273 +lemma path_components_of_eq_empty:
   7.274 +   "path_components_of X = {} \<longleftrightarrow> topspace X = {}"
   7.275 +  using Union_path_components_of nonempty_path_components_of by fastforce
   7.276 +
   7.277 +lemma path_components_of_empty_space:
   7.278 +   "topspace X = {} \<Longrightarrow> path_components_of X = {}"
   7.279 +  by (simp add: path_components_of_eq_empty)
   7.280 +
   7.281 +lemma path_components_of_subset_singleton:
   7.282 +  "path_components_of X \<subseteq> {S} \<longleftrightarrow>
   7.283 +        path_connected_space X \<and> (topspace X = {} \<or> topspace X = S)"
   7.284 +proof (cases "topspace X = {}")
   7.285 +  case True
   7.286 +  then show ?thesis
   7.287 +    by (auto simp: path_components_of_empty_space path_connected_space_topspace_empty)
   7.288 +next
   7.289 +  case False
   7.290 +  have "(path_components_of X = {S}) \<longleftrightarrow> (path_connected_space X \<and> topspace X = S)"
   7.291 +  proof (intro iffI conjI)
   7.292 +    assume L: "path_components_of X = {S}"
   7.293 +    then show "path_connected_space X"
   7.294 +      by (simp add: path_connected_space_iff_components_eq)
   7.295 +    show "topspace X = S"
   7.296 +      by (metis L ccpo_Sup_singleton [of S] Union_path_components_of)
   7.297 +  next
   7.298 +    assume R: "path_connected_space X \<and> topspace X = S"
   7.299 +    then show "path_components_of X = {S}"
   7.300 +      using ccpo_Sup_singleton [of S]
   7.301 +      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)
   7.302 +  qed
   7.303 +  with False show ?thesis
   7.304 +    by (simp add: path_components_of_eq_empty subset_singleton_iff)
   7.305 +qed
   7.306 +
   7.307 +lemma path_connected_space_iff_components_subset_singleton:
   7.308 +   "path_connected_space X \<longleftrightarrow> (\<exists>a. path_components_of X \<subseteq> {a})"
   7.309 +  by (simp add: path_components_of_subset_singleton)
   7.310 +
   7.311 +lemma path_components_of_eq_singleton:
   7.312 +   "path_components_of X = {S} \<longleftrightarrow> path_connected_space X \<and> topspace X \<noteq> {} \<and> S = topspace X"
   7.313 +  by (metis cSup_singleton insert_not_empty path_components_of_subset_singleton subset_singleton_iff)
   7.314 +
   7.315 +lemma path_components_of_path_connected_space:
   7.316 +   "path_connected_space X \<Longrightarrow> path_components_of X = (if topspace X = {} then {} else {topspace X})"
   7.317 +  by (simp add: path_components_of_eq_empty path_components_of_eq_singleton)
   7.318 +
   7.319 +lemma path_component_subset_connected_component_of:
   7.320 +   "path_component_of_set X x \<subseteq> connected_component_of_set X x"
   7.321 +proof (cases "x \<in> topspace X")
   7.322 +  case True
   7.323 +  then show ?thesis
   7.324 +    by (simp add: connected_component_of_maximal path_component_of_refl path_connectedin_imp_connectedin path_connectedin_path_component_of)
   7.325 +next
   7.326 +  case False
   7.327 +  then show ?thesis
   7.328 +    using path_component_of_eq_empty by fastforce
   7.329 +qed
   7.330 +
   7.331 +lemma exists_path_component_of_superset:
   7.332 +  assumes S: "path_connectedin X S" and ne: "topspace X \<noteq> {}"
   7.333 +  obtains C where "C \<in> path_components_of X" "S \<subseteq> C"
   7.334 +proof (cases "S = {}")
   7.335 +  case True
   7.336 +  then show ?thesis
   7.337 +    using ne path_components_of_eq_empty that by fastforce
   7.338 +next
   7.339 +  case False
   7.340 +  then obtain a where "a \<in> S"
   7.341 +    by blast
   7.342 +  show ?thesis
   7.343 +  proof
   7.344 +    show "Collect (path_component_of X a) \<in> path_components_of X"
   7.345 +      by (meson \<open>a \<in> S\<close> S subsetD path_component_in_path_components_of path_connectedin_subset_topspace)
   7.346 +    show "S \<subseteq> Collect (path_component_of X a)"
   7.347 +      by (simp add: S \<open>a \<in> S\<close> path_component_of_maximal)
   7.348 +  qed
   7.349 +qed
   7.350 +
   7.351 +lemma path_component_of_eq_overlap:
   7.352 +   "path_component_of X x = path_component_of X y \<longleftrightarrow>
   7.353 +      (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
   7.354 +      Collect (path_component_of X x) \<inter> Collect (path_component_of X y) \<noteq> {}"
   7.355 +  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)
   7.356 +
   7.357 +lemma path_component_of_nonoverlap:
   7.358 +   "Collect (path_component_of X x) \<inter> Collect (path_component_of X y) = {} \<longleftrightarrow>
   7.359 +    (x \<notin> topspace X) \<or> (y \<notin> topspace X) \<or>
   7.360 +    path_component_of X x \<noteq> path_component_of X y"
   7.361 +  by (metis inf.idem path_component_of_eq_empty path_component_of_eq_overlap)
   7.362 +
   7.363 +lemma path_component_of_overlap:
   7.364 +   "Collect (path_component_of X x) \<inter> Collect (path_component_of X y) \<noteq> {} \<longleftrightarrow>
   7.365 +    x \<in> topspace X \<and> y \<in> topspace X \<and> path_component_of X x = path_component_of X y"
   7.366 +  by (meson path_component_of_nonoverlap)
   7.367 +
   7.368 +lemma path_components_of_disjoint:
   7.369 +     "\<lbrakk>C \<in> path_components_of X; C' \<in> path_components_of X\<rbrakk> \<Longrightarrow> disjnt C C' \<longleftrightarrow> C \<noteq> C'"
   7.370 +  by (auto simp: path_components_of_def path_component_of_disjoint path_component_of_equiv)
   7.371 +
   7.372 +lemma path_components_of_overlap:
   7.373 +    "\<lbrakk>C \<in> path_components_of X; C' \<in> path_components_of X\<rbrakk> \<Longrightarrow> C \<inter> C' \<noteq> {} \<longleftrightarrow> C = C'"
   7.374 +  by (auto simp: path_components_of_def path_component_of_equiv)
   7.375 +
   7.376 +lemma path_component_of_unique:
   7.377 +   "\<lbrakk>x \<in> C; path_connectedin X C; \<And>C'. \<lbrakk>x \<in> C'; path_connectedin X C'\<rbrakk> \<Longrightarrow> C' \<subseteq> C\<rbrakk>
   7.378 +        \<Longrightarrow> Collect (path_component_of X x) = C"
   7.379 +  by (meson subsetD eq_iff path_component_of_maximal path_connectedin_path_component_of)
   7.380 +
   7.381 +lemma path_component_of_discrete_topology [simp]:
   7.382 +  "Collect (path_component_of (discrete_topology U) x) = (if x \<in> U then {x} else {})"
   7.383 +proof -
   7.384 +  have "\<And>C'. \<lbrakk>x \<in> C'; path_connectedin (discrete_topology U) C'\<rbrakk> \<Longrightarrow> C' \<subseteq> {x}"
   7.385 +    by (metis path_connectedin_discrete_topology subsetD singletonD)
   7.386 +  then have "x \<in> U \<Longrightarrow> Collect (path_component_of (discrete_topology U) x) = {x}"
   7.387 +    by (simp add: path_component_of_unique)
   7.388 +  then show ?thesis
   7.389 +    using path_component_in_topspace by fastforce
   7.390 +qed
   7.391 +
   7.392 +lemma path_component_of_discrete_topology_iff [simp]:
   7.393 +  "path_component_of (discrete_topology U) x y \<longleftrightarrow> x \<in> U \<and> y=x"
   7.394 +  by (metis empty_iff insertI1 mem_Collect_eq path_component_of_discrete_topology singletonD)
   7.395 +
   7.396 +lemma path_components_of_discrete_topology [simp]:
   7.397 +   "path_components_of (discrete_topology U) = (\<lambda>x. {x}) ` U"
   7.398 +  by (auto simp: path_components_of_def image_def fun_eq_iff)
   7.399 +
   7.400 +lemma homeomorphic_map_path_component_of:
   7.401 +  assumes f: "homeomorphic_map X Y f" and x: "x \<in> topspace X"
   7.402 +  shows "Collect (path_component_of Y (f x)) = f ` Collect(path_component_of X x)"
   7.403 +proof -
   7.404 +  obtain g where g: "homeomorphic_maps X Y f g"
   7.405 +    using f homeomorphic_map_maps by blast
   7.406 +  show ?thesis
   7.407 +  proof
   7.408 +    have "Collect (path_component_of Y (f x)) \<subseteq> topspace Y"
   7.409 +      by (simp add: path_component_of_subset_topspace)
   7.410 +    moreover have "g ` Collect(path_component_of Y (f x)) \<subseteq> Collect (path_component_of X (g (f x)))"
   7.411 +      using g x unfolding homeomorphic_maps_def
   7.412 +      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)
   7.413 +    ultimately show "Collect (path_component_of Y (f x)) \<subseteq> f ` Collect (path_component_of X x)"
   7.414 +      using g x unfolding homeomorphic_maps_def continuous_map_def image_iff subset_iff
   7.415 +      by metis
   7.416 +    show "f ` Collect (path_component_of X x) \<subseteq> Collect (path_component_of Y (f x))"
   7.417 +    proof (rule path_component_of_maximal)
   7.418 +      show "path_connectedin Y (f ` Collect (path_component_of X x))"
   7.419 +        by (meson f homeomorphic_map_path_connectedness_eq path_connectedin_path_component_of)
   7.420 +    qed (simp add: path_component_of_refl x)
   7.421 +  qed
   7.422 +qed
   7.423 +
   7.424 +lemma homeomorphic_map_path_components_of:
   7.425 +  assumes "homeomorphic_map X Y f"
   7.426 +  shows "path_components_of Y = (image f) ` (path_components_of X)"
   7.427 +  unfolding path_components_of_def homeomorphic_imp_surjective_map [OF assms, symmetric]
   7.428 +  apply safe
   7.429 +  using assms homeomorphic_map_path_component_of apply fastforce
   7.430 +  by (metis assms homeomorphic_map_path_component_of imageI)
   7.431 +
   7.432 +
   7.433  subsection \<open>Sphere is path-connected\<close>
   7.434  
   7.435  lemma path_connected_punctured_universe:
   7.436 @@ -2078,7 +2474,7 @@
   7.437          done
   7.438      }
   7.439      then have pcx: "path_component (- s) x (a + C *\<^sub>R (x - a))"
   7.440 -      by (force simp: closed_segment_def intro!: path_connected_linepath)
   7.441 +      by (force simp: closed_segment_def intro!: path_component_linepath)
   7.442      define D where "D = B / norm(y - a)"  \<comment> \<open>massive duplication with the proof above\<close>
   7.443      { fix u
   7.444        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"
   7.445 @@ -2113,7 +2509,7 @@
   7.446          done
   7.447      }
   7.448      then have pdy: "path_component (- s) y (a + D *\<^sub>R (y - a))"
   7.449 -      by (force simp: closed_segment_def intro!: path_connected_linepath)
   7.450 +      by (force simp: closed_segment_def intro!: path_component_linepath)
   7.451      have pyx: "path_component (- s) (a + D *\<^sub>R (y - a)) (a + C *\<^sub>R (x - a))"
   7.452        apply (rule path_component_of_subset [of "sphere a B"])
   7.453         using \<open>s \<subseteq> ball a B\<close>
     8.1 --- a/src/HOL/Analysis/Product_Topology.thy	Wed Mar 20 23:06:51 2019 +0100
     8.2 +++ b/src/HOL/Analysis/Product_Topology.thy	Thu Mar 21 14:18:22 2019 +0000
     8.3 @@ -1,15 +1,12 @@
     8.4 +section\<open>The binary product topology\<close>
     8.5 +
     8.6  theory Product_Topology
     8.7  imports Function_Topology   
     8.8  begin
     8.9  
    8.10 -lemma subset_UnE: (*FIXME MOVE*)
    8.11 -  assumes "C \<subseteq> A \<union> B"
    8.12 -    obtains A' B' where "A' \<subseteq> A" "B' \<subseteq> B" "C = A' \<union> B'"
    8.13 -  by (metis assms Int_Un_distrib inf.order_iff inf_le2)
    8.14 -
    8.15  section \<open>Product Topology\<close> 
    8.16  
    8.17 -subsection\<open>A binary product topology where the two types can be different.\<close>
    8.18 +subsection\<open>Definition\<close>
    8.19  
    8.20  definition prod_topology :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<times> 'b) topology" where
    8.21   "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}))"
    8.22 @@ -34,7 +31,7 @@
    8.23  proof (rule topology_inverse')
    8.24    show "istopology (arbitrary union_of (\<lambda>U. U \<in> {S \<times> T |S T. openin X S \<and> openin Y T}))"
    8.25      apply (rule istopology_base, simp)
    8.26 -    by (metis openin_Int times_Int_times)
    8.27 +    by (metis openin_Int Times_Int_Times)
    8.28  qed
    8.29  
    8.30  lemma topspace_prod_topology [simp]:
    8.31 @@ -62,7 +59,7 @@
    8.32  proof -
    8.33    have "((\<lambda>U. \<exists>S T. U = S \<times> T \<and> openin X S \<and> openin Y T) relative_to S \<times> T) =
    8.34          (\<lambda>U. \<exists>S' T'. U = S' \<times> T' \<and> (openin X relative_to S) S' \<and> (openin Y relative_to T) T')"
    8.35 -    by (auto simp: relative_to_def times_Int_times fun_eq_iff) metis
    8.36 +    by (auto simp: relative_to_def Times_Int_Times fun_eq_iff) metis
    8.37    then show ?thesis
    8.38      by (simp add: topology_eq openin_prod_topology arbitrary_union_of_relative_to flip: openin_relative_to)
    8.39  qed
    8.40 @@ -81,7 +78,7 @@
    8.41  
    8.42  lemma prod_topology_subtopology_eu [simp]:
    8.43    "prod_topology (subtopology euclidean S) (subtopology euclidean T) = subtopology euclidean (S \<times> T)"
    8.44 -  by (simp add: prod_topology_subtopology subtopology_subtopology times_Int_times)
    8.45 +  by (simp add: prod_topology_subtopology subtopology_subtopology Times_Int_Times)
    8.46  
    8.47  lemma continuous_map_subtopology_eu [simp]:
    8.48    "continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
    8.49 @@ -128,6 +125,29 @@
    8.50     "closedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> closedin X S \<and> closedin Y T"
    8.51    by (auto simp: closure_of_Times times_eq_iff simp flip: closure_of_eq)
    8.52  
    8.53 +lemma interior_of_Times: "(prod_topology X Y) interior_of (S \<times> T) = (X interior_of S) \<times> (Y interior_of T)"
    8.54 +proof (rule interior_of_unique)
    8.55 +  show "(X interior_of S) \<times> Y interior_of T \<subseteq> S \<times> T"
    8.56 +    by (simp add: Sigma_mono interior_of_subset)
    8.57 +  show "openin (prod_topology X Y) ((X interior_of S) \<times> Y interior_of T)"
    8.58 +    by (simp add: openin_Times)
    8.59 +next
    8.60 +  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'
    8.61 +  proof (clarsimp; intro conjI)
    8.62 +    fix a :: "'a" and b :: "'b"
    8.63 +    assume "(a, b) \<in> T'"
    8.64 +    with that obtain U V where UV: "openin X U" "openin Y V" "a \<in> U" "b \<in> V" "U \<times> V \<subseteq> T'"
    8.65 +      by (metis openin_prod_topology_alt)
    8.66 +    then show "a \<in> X interior_of S"
    8.67 +      using interior_of_maximal_eq that(1) by fastforce
    8.68 +    show "b \<in> Y interior_of T"
    8.69 +      using UV interior_of_maximal_eq that(1)
    8.70 +      by (metis SigmaI mem_Sigma_iff subset_eq)
    8.71 +  qed
    8.72 +qed
    8.73 +
    8.74 +subsection \<open>Continuity\<close>
    8.75 +
    8.76  lemma continuous_map_pairwise:
    8.77     "continuous_map Z (prod_topology X Y) f \<longleftrightarrow> continuous_map Z X (fst \<circ> f) \<and> continuous_map Z Y (snd \<circ> f)"
    8.78     (is "?lhs = ?rhs")
    8.79 @@ -297,37 +317,6 @@
    8.80      by (simp add: continuous_map_paired case_prod_unfold continuous_map_of_fst [unfolded o_def] continuous_map_of_snd [unfolded o_def])
    8.81  qed
    8.82  
    8.83 -lemma homeomorphic_maps_prod:
    8.84 -   "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>
    8.85 -        topspace(prod_topology X Y) = {} \<and>
    8.86 -        topspace(prod_topology X' Y') = {} \<or>
    8.87 -        homeomorphic_maps X X' f f' \<and>
    8.88 -        homeomorphic_maps Y Y' g g'"
    8.89 -  unfolding homeomorphic_maps_def continuous_map_prod_top
    8.90 -  by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
    8.91 -
    8.92 -lemma embedding_map_graph:
    8.93 -   "embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
    8.94 -    (is "?lhs = ?rhs")
    8.95 -proof
    8.96 -  assume L: ?lhs
    8.97 -  have "snd \<circ> (\<lambda>x. (x, f x)) = f"
    8.98 -    by force
    8.99 -  moreover have "continuous_map X Y (snd \<circ> (\<lambda>x. (x, f x)))"
   8.100 -    using L
   8.101 -    unfolding embedding_map_def
   8.102 -    by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map)
   8.103 -  ultimately show ?rhs
   8.104 -    by simp
   8.105 -next
   8.106 -  assume R: ?rhs
   8.107 -  then show ?lhs
   8.108 -    unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def
   8.109 -    by (rule_tac x=fst in exI)
   8.110 -       (auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology
   8.111 -                   continuous_map_fst topspace_subtopology)
   8.112 -qed
   8.113 -
   8.114  lemma in_prod_topology_closure_of:
   8.115    assumes  "z \<in> (prod_topology X Y) closure_of S"
   8.116    shows "fst z \<in> X closure_of (fst ` S)" "snd z \<in> Y closure_of (snd ` S)"
   8.117 @@ -412,7 +401,7 @@
   8.118            then show ?case
   8.119              unfolding \<X>_def \<Y>_def
   8.120              apply (simp add: Int_ac subset_eq image_def)
   8.121 -            apply (metis (no_types) openin_Int openin_topspace times_Int_times)
   8.122 +            apply (metis (no_types) openin_Int openin_topspace Times_Int_Times)
   8.123              done
   8.124          qed auto
   8.125          then show ?thesis
   8.126 @@ -450,10 +439,85 @@
   8.127      using False by blast
   8.128  qed
   8.129  
   8.130 -
   8.131  lemma compactin_Times:
   8.132     "compactin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> compactin X S \<and> compactin Y T"
   8.133    by (auto simp: compactin_subspace subtopology_Times compact_space_prod_topology)
   8.134  
   8.135 +subsection\<open>Homeomorphic maps\<close>
   8.136 +
   8.137 +lemma homeomorphic_maps_prod:
   8.138 +   "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>
   8.139 +        topspace(prod_topology X Y) = {} \<and>
   8.140 +        topspace(prod_topology X' Y') = {} \<or>
   8.141 +        homeomorphic_maps X X' f f' \<and>
   8.142 +        homeomorphic_maps Y Y' g g'"
   8.143 +  unfolding homeomorphic_maps_def continuous_map_prod_top
   8.144 +  by (auto simp: continuous_map_def homeomorphic_maps_def continuous_map_prod_top)
   8.145 +
   8.146 +lemma embedding_map_graph:
   8.147 +   "embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
   8.148 +    (is "?lhs = ?rhs")
   8.149 +proof
   8.150 +  assume L: ?lhs
   8.151 +  have "snd \<circ> (\<lambda>x. (x, f x)) = f"
   8.152 +    by force
   8.153 +  moreover have "continuous_map X Y (snd \<circ> (\<lambda>x. (x, f x)))"
   8.154 +    using L
   8.155 +    unfolding embedding_map_def
   8.156 +    by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map)
   8.157 +  ultimately show ?rhs
   8.158 +    by simp
   8.159 +next
   8.160 +  assume R: ?rhs
   8.161 +  then show ?lhs
   8.162 +    unfolding homeomorphic_map_maps embedding_map_def homeomorphic_maps_def
   8.163 +    by (rule_tac x=fst in exI)
   8.164 +       (auto simp: continuous_map_in_subtopology continuous_map_paired continuous_map_from_subtopology
   8.165 +                   continuous_map_fst topspace_subtopology)
   8.166 +qed
   8.167 +
   8.168 +lemma homeomorphic_space_prod_topology:
   8.169 +   "\<lbrakk>X homeomorphic_space X''; Y homeomorphic_space Y'\<rbrakk>
   8.170 +        \<Longrightarrow> prod_topology X Y homeomorphic_space prod_topology X'' Y'"
   8.171 +using homeomorphic_maps_prod unfolding homeomorphic_space_def by blast
   8.172 +
   8.173 +lemma prod_topology_homeomorphic_space_left:
   8.174 +   "topspace Y = {b} \<Longrightarrow> prod_topology X Y homeomorphic_space X"
   8.175 +  unfolding homeomorphic_space_def
   8.176 +  by (rule_tac x=fst in exI) (simp add: homeomorphic_map_def inj_on_def flip: homeomorphic_map_maps)
   8.177 +
   8.178 +lemma prod_topology_homeomorphic_space_right:
   8.179 +   "topspace X = {a} \<Longrightarrow> prod_topology X Y homeomorphic_space Y"
   8.180 +  unfolding homeomorphic_space_def
   8.181 +  by (rule_tac x=snd in exI) (simp add: homeomorphic_map_def inj_on_def flip: homeomorphic_map_maps)
   8.182 +
   8.183 +
   8.184 +lemma homeomorphic_space_prod_topology_sing1:
   8.185 +     "b \<in> topspace Y \<Longrightarrow> X homeomorphic_space (prod_topology X (subtopology Y {b}))"
   8.186 +  by (metis empty_subsetI homeomorphic_space_sym inf.absorb_iff2 insert_subset prod_topology_homeomorphic_space_left topspace_subtopology)
   8.187 +
   8.188 +lemma homeomorphic_space_prod_topology_sing2:
   8.189 +     "a \<in> topspace X \<Longrightarrow> Y homeomorphic_space (prod_topology (subtopology X {a}) Y)"
   8.190 +  by (metis empty_subsetI homeomorphic_space_sym inf.absorb_iff2 insert_subset prod_topology_homeomorphic_space_right topspace_subtopology)
   8.191 +
   8.192 +lemma topological_property_of_prod_component:
   8.193 +  assumes major: "P(prod_topology X Y)"
   8.194 +    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))"
   8.195 +    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}))"
   8.196 +    and PQ:  "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
   8.197 +    and PR: "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> R X')"
   8.198 +  shows "topspace(prod_topology X Y) = {} \<or> Q X \<and> R Y"
   8.199 +proof -
   8.200 +  have "Q X \<and> R Y" if "topspace(prod_topology X Y) \<noteq> {}"
   8.201 +  proof -
   8.202 +    from that obtain a b where a: "a \<in> topspace X" and b: "b \<in> topspace Y"
   8.203 +      by force
   8.204 +    show ?thesis
   8.205 +      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]
   8.206 +      by (simp add: subtopology_Times) (meson PQ PR homeomorphic_space_prod_topology_sing2 homeomorphic_space_sym)
   8.207 +  qed
   8.208 +  then show ?thesis by metis
   8.209 +qed
   8.210 +
   8.211  end
   8.212  
     9.1 --- a/src/HOL/Analysis/T1_Spaces.thy	Wed Mar 20 23:06:51 2019 +0100
     9.2 +++ b/src/HOL/Analysis/T1_Spaces.thy	Thu Mar 21 14:18:22 2019 +0000
     9.3 @@ -1,7 +1,7 @@
     9.4  section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
     9.5  
     9.6  theory T1_Spaces
     9.7 -imports Function_Topology 
     9.8 +imports Product_Topology 
     9.9  begin
    9.10  
    9.11  definition t1_space where
    9.12 @@ -198,4 +198,20 @@
    9.13      using False by blast
    9.14  qed
    9.15  
    9.16 +lemma t1_space_prod_topology:
    9.17 +   "t1_space(prod_topology X Y) \<longleftrightarrow> topspace(prod_topology X Y) = {} \<or> t1_space X \<and> t1_space Y"
    9.18 +proof (cases "topspace (prod_topology X Y) = {}")
    9.19 +  case True then show ?thesis
    9.20 +  by (auto simp: t1_space_empty)
    9.21 +next
    9.22 +  case False
    9.23 +  have eq: "{(x,y)} = {x} \<times> {y}" for x y
    9.24 +    by simp
    9.25 +  have "t1_space (prod_topology X Y) \<longleftrightarrow> (t1_space X \<and> t1_space Y)"
    9.26 +    using False
    9.27 +    by (force simp: t1_space_closedin_singleton closedin_Times eq simp del: insert_Times_insert)
    9.28 +  with False show ?thesis
    9.29 +    by simp
    9.30 +qed
    9.31 +
    9.32  end
    10.1 --- a/src/HOL/Library/FuncSet.thy	Wed Mar 20 23:06:51 2019 +0100
    10.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Mar 21 14:18:22 2019 +0000
    10.3 @@ -550,6 +550,11 @@
    10.4  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})"
    10.5    by (metis (mono_tags, lifting) PiE_eq PiE_singleton insert_not_empty restrict_apply' restrict_extensional)
    10.6  
    10.7 +lemma PiE_over_singleton_iff: "(\<Pi>\<^sub>E x\<in>{a}. B x) = (\<Union>b \<in> B a. {\<lambda>x \<in> {a}. b})"
    10.8 +  apply (auto simp: PiE_iff split: if_split_asm)
    10.9 +  apply (metis (no_types, lifting) extensionalityI restrict_apply' restrict_extensional singletonD)
   10.10 +  done
   10.11 +
   10.12  lemma all_PiE_elements:
   10.13     "(\<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")
   10.14  proof (cases "PiE I S = {}")
    11.1 --- a/src/HOL/Product_Type.thy	Wed Mar 20 23:06:51 2019 +0100
    11.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 21 14:18:22 2019 +0000
    11.3 @@ -1134,7 +1134,7 @@
    11.4      by (cases "f x") (auto split: prod.split)
    11.5  qed
    11.6  
    11.7 -lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
    11.8 +lemma Times_Int_Times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
    11.9    by auto
   11.10  
   11.11  lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A"
    12.1 --- a/src/HOL/Set.thy	Wed Mar 20 23:06:51 2019 +0100
    12.2 +++ b/src/HOL/Set.thy	Thu Mar 21 14:18:22 2019 +0000
    12.3 @@ -1354,6 +1354,13 @@
    12.4  lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
    12.5    by blast
    12.6  
    12.7 +lemma subset_UnE: 
    12.8 +  assumes "C \<subseteq> A \<union> B"
    12.9 +  obtains A' B' where "A' \<subseteq> A" "B' \<subseteq> B" "C = A' \<union> B'"
   12.10 +proof
   12.11 +  show "C \<inter> A \<subseteq> A" "C \<inter> B \<subseteq> B" "C = (C \<inter> A) \<union> (C \<inter> B)"
   12.12 +    using assms by blast+
   12.13 +qed
   12.14  
   12.15  text \<open>\<^medskip> Set complement\<close>
   12.16  
   12.17 @@ -1594,6 +1601,9 @@
   12.18    "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
   12.19    by auto
   12.20  
   12.21 +lemma ex_image_cong_iff [simp, no_atp]:
   12.22 +  "(\<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))"
   12.23 +  by auto
   12.24  
   12.25  subsubsection \<open>Monotonicity of various operations\<close>
   12.26