# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1684167138 -3600
# Node ID 37894dff0111101415bedcc88781707580944b06
# Parent  2594319ad9eec33e6736cf87e7383364302a4ebb
More material from the HOL Light metric space library

diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Thu May 11 22:12:43 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Mon May 15 17:12:18 2023 +0100
@@ -71,69 +71,6 @@
   by (simp add: Hausdorff_imp_t1_space connectedin_imp_perfect_gen)
 
 
-proposition connected_space_prod_topology:
-   "connected_space(prod_topology X Y) \<longleftrightarrow>
-    topspace(prod_topology X Y) = {} \<or> connected_space X \<and> connected_space Y" (is "?lhs=?rhs")
-proof (cases "topspace(prod_topology X Y) = {}")
-  case True
-  then show ?thesis
-    using connected_space_topspace_empty by blast
-next
-  case False
-  then have nonempty: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
-    by force+
-  show ?thesis 
-  proof
-    assume ?lhs
-    then show ?rhs
-      by (meson connected_space_quotient_map_image nonempty quotient_map_fst quotient_map_snd)
-  next
-    assume ?rhs
-    then have conX: "connected_space X" and conY: "connected_space Y"
-      using False by blast+
-    have False
-      if "openin (prod_topology X Y) U" and "openin (prod_topology X Y) V"
-        and UV: "topspace X \<times> topspace Y \<subseteq> U \<union> V" "U \<inter> V = {}" 
-        and "U \<noteq> {}" and "V \<noteq> {}"
-      for U V
-    proof -
-      have Usub: "U \<subseteq> topspace X \<times> topspace Y" and Vsub: "V \<subseteq> topspace X \<times> topspace Y"
-        using that by (metis openin_subset topspace_prod_topology)+
-      obtain a b where ab: "(a,b) \<in> U" and a: "a \<in> topspace X" and b: "b \<in> topspace Y"
-        using \<open>U \<noteq> {}\<close> Usub by auto
-      have "\<not> topspace X \<times> topspace Y \<subseteq> U"
-        using Usub Vsub \<open>U \<inter> V = {}\<close> \<open>V \<noteq> {}\<close> by auto
-      then obtain x y where x: "x \<in> topspace X" and y: "y \<in> topspace Y" and "(x,y) \<notin> U"
-        by blast
-      have oX: "openin X {x \<in> topspace X. (x,y) \<in> U}" "openin X {x \<in> topspace X. (x,y) \<in> V}"
-       and oY: "openin Y {y \<in> topspace Y. (a,y) \<in> U}" "openin Y {y \<in> topspace Y. (a,y) \<in> V}"
-        by (force intro: openin_continuous_map_preimage [where Y = "prod_topology X Y"] 
-            simp: that continuous_map_pairwise o_def x y a)+
-      have 1: "topspace Y \<subseteq> {y \<in> topspace Y. (a,y) \<in> U} \<union> {y \<in> topspace Y. (a,y) \<in> V}"
-        using a that(3) by auto
-      have 2: "{y \<in> topspace Y. (a,y) \<in> U} \<inter> {y \<in> topspace Y. (a,y) \<in> V} = {}"
-        using that(4) by auto
-      have 3: "{y \<in> topspace Y. (a,y) \<in> U} \<noteq> {}"
-        using ab b by auto
-      have 4: "{y \<in> topspace Y. (a,y) \<in> V} \<noteq> {}"
-      proof -
-        show ?thesis
-          using connected_spaceD [OF conX oX] UV \<open>(x,y) \<notin> U\<close> a x y
-                disjoint_iff_not_equal by blast
-      qed
-      show ?thesis
-        using connected_spaceD [OF conY oY 1 2 3 4] by auto
-    qed
-    then show ?lhs
-      unfolding connected_space_def topspace_prod_topology by blast 
-  qed
-qed
-
-lemma connectedin_Times:
-   "connectedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow>
-        S = {} \<or> T = {} \<or> connectedin X S \<and> connectedin Y T"
-  by (force simp: connectedin_def subtopology_Times connected_space_prod_topology)
-
 
 subsection\<open>The notion of "separated between" (complement of "connected between)"\<close>
 
diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Thu May 11 22:12:43 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Mon May 15 17:12:18 2023 +0100
@@ -296,6 +296,10 @@
   unfolding closedin_def topspace_subtopology
   by (auto simp: openin_subtopology)
 
+lemma closedin_subset_topspace:
+   "\<lbrakk>closedin X S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology X T) S"
+  using closedin_subtopology by fastforce
+
 lemma closedin_relative_to:
    "(closedin X relative_to S) = closedin (subtopology X S)"
   by (force simp: relative_to_def closedin_subtopology)
@@ -3378,6 +3382,10 @@
   qed
 qed
 
+lemma connected_space_quotient_map_image:
+   "\<lbrakk>quotient_map X X' q; connected_space X\<rbrakk> \<Longrightarrow> connected_space X'"
+  by (metis connectedin_continuous_map_image connectedin_topspace quotient_imp_continuous_map quotient_imp_surjective_map)
+
 lemma homeomorphic_connected_space:
      "X homeomorphic_space Y \<Longrightarrow> connected_space X \<longleftrightarrow> connected_space Y"
   unfolding homeomorphic_space_def homeomorphic_maps_def
diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Thu May 11 22:12:43 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Mon May 15 17:12:18 2023 +0100
@@ -1639,4 +1639,53 @@
      (\<lambda>x. x / (1 + \<bar>x\<bar>))  (\<lambda>y. y / (1 - \<bar>y\<bar>))"
   by (force simp: homeomorphic_maps_def continuous_map_real_shrink continuous_on_real_grow divide_simps)
 
+lemma real_shrink_Galois:
+  fixes x::real
+  shows "(x / (1 + \<bar>x\<bar>) = y) \<longleftrightarrow> (\<bar>y\<bar> < 1 \<and> y / (1 - \<bar>y\<bar>) = x)"
+  using real_grow_shrink by (fastforce simp add: distrib_left)
+
+lemma real_shrink_lt:
+  fixes x::real
+  shows "x / (1 + \<bar>x\<bar>) < y / (1 + \<bar>y\<bar>) \<longleftrightarrow> x < y"
+  using zero_less_mult_iff [of x y] by (auto simp: field_simps abs_if not_less)
+
+lemma real_shrink_le:
+  fixes x::real
+  shows "x / (1 + \<bar>x\<bar>) \<le> y / (1 + \<bar>y\<bar>) \<longleftrightarrow> x \<le> y"
+  by (meson linorder_not_le real_shrink_lt)
+
+lemma real_shrink_grow:
+  fixes x::real
+  shows "\<bar>x\<bar> < 1 \<Longrightarrow> x / (1 - \<bar>x\<bar>) / (1 + \<bar>x / (1 - \<bar>x\<bar>)\<bar>) = x"
+  using real_shrink_Galois by blast
+
+lemma continuous_shrink:
+  "continuous_on UNIV (\<lambda>x::real. x / (1 + \<bar>x\<bar>))"
+  by (intro continuous_intros) auto
+
+lemma strict_mono_shrink:
+  "strict_mono (\<lambda>x::real. x / (1 + \<bar>x\<bar>))"
+  by (simp add: monotoneI real_shrink_lt)
+
+lemma shrink_range: "(\<lambda>x::real. x / (1 + \<bar>x\<bar>)) ` S \<subseteq> {-1<..<1}"
+  by (auto simp: divide_simps)
+
+text \<open>Note: connected sets of real numbers are the same thing as intervals\<close>
+lemma connected_shrink:
+  fixes S :: "real set"
+  shows "connected ((\<lambda>x. x / (1 + \<bar>x\<bar>)) ` S) \<longleftrightarrow> connected S"  (is "?lhs = ?rhs")
+proof 
+  assume "?lhs"
+  then have "connected ((\<lambda>x. x / (1 - \<bar>x\<bar>)) ` (\<lambda>x. x / (1 + \<bar>x\<bar>)) ` S)"
+    by (metis continuous_on_real_grow shrink_range connected_continuous_image 
+               continuous_on_subset)
+  then show "?rhs"
+    using real_grow_shrink by (force simp add: image_comp)
+next
+  assume ?rhs
+  then show ?lhs
+    using connected_continuous_image 
+    by (metis continuous_on_subset continuous_shrink subset_UNIV)
+qed
+
 end
\ No newline at end of file
diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu May 11 22:12:43 2023 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon May 15 17:12:18 2023 +0100
@@ -437,6 +437,9 @@
   by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior
       subset_trans)
 
+lemma ball_iff_cball: "(\<exists>r>0. ball x r \<subseteq> U) \<longleftrightarrow> (\<exists>r>0. cball x r \<subseteq> U)"
+  by (meson mem_interior mem_interior_cball)
+
 
 subsection \<open>Frontier\<close>
 
diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Locally.thy
--- a/src/HOL/Analysis/Locally.thy	Thu May 11 22:12:43 2023 +0200
+++ b/src/HOL/Analysis/Locally.thy	Mon May 15 17:12:18 2023 +0100
@@ -2,7 +2,7 @@
 
 theory Locally
   imports
-    Path_Connected Function_Topology
+    Path_Connected Function_Topology Sum_Topology
 begin
 
 subsection\<open>Neighbourhood Bases\<close>
@@ -448,4 +448,525 @@
     using False by blast
 qed
 
+lemma locally_path_connected_is_realinterval:
+  assumes "is_interval S"
+  shows "locally_path_connected_space(subtopology euclideanreal S)"
+  unfolding locally_path_connected_space_def
+proof (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt)
+  fix a U
+  assume "a \<in> S" and "a \<in> U" and "open U"
+  then obtain r where "r > 0" and r: "ball a r \<subseteq> U"
+    by (metis open_contains_ball_eq)
+  show "\<exists>W. open W \<and> (\<exists>V. path_connectedin (top_of_set S) V \<and> a \<in> W \<and> S \<inter> W \<subseteq> V \<and> V \<subseteq> S \<and> V \<subseteq> U)"
+  proof (intro exI conjI)
+    show "path_connectedin (top_of_set S) (S \<inter> ball a r)"
+      by (simp add: assms is_interval_Int is_interval_ball_real is_interval_path_connected path_connectedin_subtopology)
+    show "a \<in> ball a r"
+      by (simp add: \<open>0 < r\<close>)
+  qed (use \<open>0 < r\<close> r in auto)
+qed
+
+lemma locally_path_connected_real_interval:
+ "locally_path_connected_space (subtopology euclideanreal{a..b})"
+  "locally_path_connected_space (subtopology euclideanreal{a<..<b})"
+  using locally_path_connected_is_realinterval
+  by (auto simp add: is_interval_1)
+
+lemma locally_path_connected_space_prod_topology:
+   "locally_path_connected_space (prod_topology X Y) \<longleftrightarrow>
+      topspace (prod_topology X Y) = {} \<or>
+      locally_path_connected_space X \<and> locally_path_connected_space Y" (is "?lhs=?rhs")
+proof (cases "topspace(prod_topology X Y) = {}")
+  case True
+  then show ?thesis
+    by (metis equals0D locally_path_connected_space_def neighbourhood_base_of_def)
+next
+  case False
+  then have ne: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
+    by simp_all
+  show ?thesis
+  proof
+    assume ?lhs then show ?rhs
+      by (metis ne locally_path_connected_space_retraction_map_image retraction_map_fst retraction_map_snd)
+  next
+    assume ?rhs
+    with False have X: "locally_path_connected_space X" and Y: "locally_path_connected_space Y"
+      by auto
+    show ?lhs
+      unfolding locally_path_connected_space_def neighbourhood_base_of
+    proof clarify
+      fix UV x y
+      assume UV: "openin (prod_topology X Y) UV" and "(x,y) \<in> UV"
+      obtain A B where W12: "openin X A \<and> openin Y B \<and> x \<in> A \<and> y \<in> B \<and> A \<times> B \<subseteq> UV"
+        using X Y by (metis UV \<open>(x,y) \<in> UV\<close> openin_prod_topology_alt)
+      then obtain C D K L
+        where "openin X C" "path_connectedin X K" "x \<in> C" "C \<subseteq> K" "K \<subseteq> A"
+          "openin Y D" "path_connectedin Y L" "y \<in> D" "D \<subseteq> L" "L \<subseteq> B"
+        by (metis X Y locally_path_connected_space)
+      with W12 \<open>openin X C\<close> \<open>openin Y D\<close>
+      show "\<exists>U V. openin (prod_topology X Y) U \<and> path_connectedin (prod_topology X Y) V \<and> (x, y) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> UV"
+        apply (rule_tac x="C \<times> D" in exI)
+        apply (rule_tac x="K \<times> L" in exI)
+        apply (auto simp: openin_prod_Times_iff path_connectedin_Times)
+        done
+    qed
+  qed
+qed
+
+lemma locally_path_connected_space_sum_topology:
+   "locally_path_connected_space(sum_topology X I) \<longleftrightarrow>
+    (\<forall>i \<in> I. locally_path_connected_space (X i))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (smt (verit) homeomorphic_locally_path_connected_space locally_path_connected_space_open_subset topological_property_of_sum_component)
+next
+  assume R: ?rhs
+  show ?lhs
+  proof (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of forall_openin_sum_topology imp_conjL)
+    fix W i x
+    assume ope: "\<forall>i\<in>I. openin (X i) (W i)" 
+      and "i \<in> I" and "x \<in> W i"
+    then obtain U V where U: "openin (X i) U" and V: "path_connectedin (X i) V" 
+           and "x \<in> U" "U \<subseteq> V" "V \<subseteq> W i"
+      by (metis R \<open>i \<in> I\<close> \<open>x \<in> W i\<close> locally_path_connected_space)
+    show "\<exists>U. openin (sum_topology X I) U \<and> (\<exists>V. path_connectedin (sum_topology X I) V \<and> (i, x) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> Sigma I W)"
+    proof (intro exI conjI)
+      show "openin (sum_topology X I) (Pair i ` U)"
+        by (meson U \<open>i \<in> I\<close> open_map_component_injection open_map_def)
+      show "path_connectedin (sum_topology X I) (Pair i ` V)"
+        by (meson V \<open>i \<in> I\<close> continuous_map_component_injection path_connectedin_continuous_map_image)
+      show "Pair i ` V \<subseteq> Sigma I W"
+        using \<open>V \<subseteq> W i\<close> \<open>i \<in> I\<close> by force
+    qed (use \<open>x \<in> U\<close> \<open>U \<subseteq> V\<close> in auto)
+  qed
+qed
+
+
+subsection\<open>Locally connected spaces\<close>
+
+definition weakly_locally_connected_at 
+  where "weakly_locally_connected_at x X \<equiv> neighbourhood_base_at x (connectedin X) X"
+
+definition locally_connected_at 
+  where "locally_connected_at x X \<equiv>
+           neighbourhood_base_at x (\<lambda>U. openin X U \<and> connectedin X U ) X"
+
+definition locally_connected_space 
+  where "locally_connected_space X \<equiv> neighbourhood_base_of (connectedin X) X"
+
+
+lemma locally_connected_A: "(\<forall>U x. openin X U \<and> x \<in> U
+              \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))
+       \<Longrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> connectedin X U) X"
+  by (smt (verit, best) connected_component_of_refl connectedin_connected_component_of connectedin_subtopology mem_Collect_eq neighbourhood_base_of openin_subset topspace_subtopology_subset)
+
+lemma locally_connected_B: "locally_connected_space X \<Longrightarrow> 
+          (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))"
+  unfolding locally_connected_space_def neighbourhood_base_of
+  apply (erule all_forward)
+  apply clarify
+  apply (subst openin_subopen)
+  by (smt (verit, ccfv_threshold) Ball_Collect connected_component_of_def connected_component_of_equiv connectedin_subtopology in_mono mem_Collect_eq)
+
+lemma locally_connected_C: "neighbourhood_base_of (\<lambda>U. openin X U \<and> connectedin X U) X \<Longrightarrow> locally_connected_space X"
+  using locally_connected_space_def neighbourhood_base_of_mono by auto
+
+
+lemma locally_connected_space_alt: 
+  "locally_connected_space X \<longleftrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> connectedin X U) X"
+  using locally_connected_A locally_connected_B locally_connected_C by blast
+
+lemma locally_connected_space_eq_open_connected_component_of:
+  "locally_connected_space X \<longleftrightarrow>
+        (\<forall>U x. openin X U \<and> x \<in> U
+              \<longrightarrow> openin X (connected_component_of_set (subtopology X U) x))"
+  by (meson locally_connected_A locally_connected_B locally_connected_C)
+
+lemma locally_connected_space:
+   "locally_connected_space X \<longleftrightarrow>
+     (\<forall>V x. openin X V \<and> x \<in> V \<longrightarrow> (\<exists>U. openin X U \<and> connectedin X U \<and> x \<in> U \<and> U \<subseteq> V))"
+  by (simp add: locally_connected_space_alt open_neighbourhood_base_of)
+
+lemma locally_path_connected_imp_locally_connected_space:
+   "locally_path_connected_space X \<Longrightarrow> locally_connected_space X"
+  by (simp add: locally_connected_space_def locally_path_connected_space_def neighbourhood_base_of_mono path_connectedin_imp_connectedin)
+
+lemma locally_connected_space_open_connected_components:
+  "locally_connected_space X \<longleftrightarrow>
+   (\<forall>U C. openin X U \<and> C \<in> connected_components_of(subtopology X U) \<longrightarrow> openin X C)"
+  apply (simp add: locally_connected_space_eq_open_connected_component_of connected_components_of_def)
+  by (smt (verit) imageE image_eqI inf.orderE inf_commute openin_subset)
+
+lemma openin_connected_component_of_locally_connected_space:
+   "locally_connected_space X \<Longrightarrow> openin X (connected_component_of_set X x)"
+  by (metis connected_component_of_eq_empty locally_connected_space_eq_open_connected_component_of openin_empty openin_topspace subtopology_topspace)
+
+lemma openin_connected_components_of_locally_connected_space:
+   "\<lbrakk>locally_connected_space X; C \<in> connected_components_of X\<rbrakk> \<Longrightarrow> openin X C"
+  by (metis locally_connected_space_open_connected_components openin_topspace subtopology_topspace)
+
+lemma weakly_locally_connected_at:
+   "weakly_locally_connected_at x X \<longleftrightarrow>
+    (\<forall>V. openin X V \<and> x \<in> V
+       \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> U \<subseteq> V \<and>
+                (\<forall>y \<in> U. \<exists>C. connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    unfolding neighbourhood_base_at_def weakly_locally_connected_at_def
+    by (meson subsetD subset_trans)
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding neighbourhood_base_at_def weakly_locally_connected_at_def
+  proof clarify
+    fix V
+    assume "openin X V" and "x \<in> V"
+    then obtain U where "openin X U" "x \<in> U" "U \<subseteq> V" 
+                  and U: "\<forall>y\<in>U. \<exists>C. connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C"
+      using R by force
+    show "\<exists>A B. openin X A \<and> connectedin X B \<and> x \<in> A \<and> A \<subseteq> B \<and> B \<subseteq> V"
+    proof (intro conjI exI)
+      show "connectedin X (connected_component_of_set (subtopology X V) x)"
+        by (meson connectedin_connected_component_of connectedin_subtopology)
+      show "U \<subseteq> connected_component_of_set (subtopology X V) x"
+        using connected_component_of_maximal U
+        by (simp add: connected_component_of_def connectedin_subtopology subsetI)
+      show "connected_component_of_set (subtopology X V) x \<subseteq> V"
+        using connected_component_of_subset_topspace by fastforce
+    qed (auto simp: \<open>x \<in> U\<close> \<open>openin X U\<close>)
+  qed
+qed
+
+lemma locally_connected_space_iff_weak:
+  "locally_connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. weakly_locally_connected_at x X)"
+  by (simp add: locally_connected_space_def neighbourhood_base_of_def weakly_locally_connected_at_def)
+
+lemma locally_connected_space_im_kleinen:
+   "locally_connected_space X \<longleftrightarrow>
+    (\<forall>V x. openin X V \<and> x \<in> V
+          \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> U \<subseteq> V \<and>
+                    (\<forall>y \<in> U. \<exists>C. connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))"
+  unfolding locally_connected_space_iff_weak weakly_locally_connected_at
+  using openin_subset subsetD by fastforce
+
+lemma locally_connected_space_open_subset:
+   "\<lbrakk>locally_connected_space X; openin X S\<rbrakk> \<Longrightarrow> locally_connected_space (subtopology X S)"
+  apply (simp add: locally_connected_space_def)
+  by (smt (verit, ccfv_threshold) connectedin_subtopology neighbourhood_base_of openin_open_subtopology subset_trans)
+
+lemma locally_connected_space_quotient_map_image:
+  assumes X: "locally_connected_space X" and f: "quotient_map X Y f"
+  shows "locally_connected_space Y"
+  unfolding locally_connected_space_open_connected_components
+proof clarify
+  fix V C
+  assume "openin Y V" and C: "C \<in> connected_components_of (subtopology Y V)"
+  then have "C \<subseteq> topspace Y"
+    using connected_components_of_subset by force
+  have ope1: "openin X {a \<in> topspace X. f a \<in> V}"
+    using \<open>openin Y V\<close> f openin_continuous_map_preimage quotient_imp_continuous_map by blast
+  define Vf where "Vf \<equiv> {z \<in> topspace X. f z \<in> V}"
+  have "openin X {x \<in> topspace X. f x \<in> C}"
+  proof (clarsimp simp: openin_subopen [where S = "{x \<in> topspace X. f x \<in> C}"])
+    fix x
+    assume "x \<in> topspace X" and "f x \<in> C"
+    show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace X. f x \<in> C}"
+    proof (intro exI conjI)
+      show "openin X (connected_component_of_set (subtopology X Vf) x)"
+        by (metis Vf_def X connected_component_of_eq_empty locally_connected_B ope1 openin_empty
+                  openin_subset topspace_subtopology_subset)
+      show x_in_conn: "x \<in> connected_component_of_set (subtopology X Vf) x"
+        using C Vf_def \<open>f x \<in> C\<close> \<open>x \<in> topspace X\<close> connected_component_of_refl connected_components_of_subset by fastforce
+      have "connected_component_of_set (subtopology X Vf) x \<subseteq> topspace X \<inter> Vf"
+        using connected_component_of_subset_topspace by fastforce
+      moreover
+      have "f ` connected_component_of_set (subtopology X Vf) x \<subseteq> C"
+      proof (rule connected_components_of_maximal [where X = "subtopology Y V"])
+        show "C \<in> connected_components_of (subtopology Y V)"
+          by (simp add: C)
+        have \<section>: "quotient_map (subtopology X Vf) (subtopology Y V) f"
+          by (simp add: Vf_def \<open>openin Y V\<close> f quotient_map_restriction)
+        then show "connectedin (subtopology Y V) (f ` connected_component_of_set (subtopology X Vf) x)"
+          by (metis connectedin_connected_component_of connectedin_continuous_map_image quotient_imp_continuous_map)
+        show "\<not> disjnt C (f ` connected_component_of_set (subtopology X Vf) x)"
+          using \<open>f x \<in> C\<close> x_in_conn by (auto simp: disjnt_iff)
+      qed
+      ultimately
+      show "connected_component_of_set (subtopology X Vf) x \<subseteq> {x \<in> topspace X. f x \<in> C}"
+        by blast
+    qed
+  qed
+  then show "openin Y C"
+    using \<open>C \<subseteq> topspace Y\<close> f quotient_map_def by fastforce
+qed
+
+
+lemma locally_connected_space_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; locally_connected_space X\<rbrakk>
+        \<Longrightarrow> locally_connected_space Y"
+  using locally_connected_space_quotient_map_image retraction_imp_quotient_map by blast
+
+lemma homeomorphic_locally_connected_space:
+   "X homeomorphic_space Y \<Longrightarrow> locally_connected_space X \<longleftrightarrow> locally_connected_space Y"
+  by (meson homeomorphic_map_def homeomorphic_space homeomorphic_space_sym locally_connected_space_quotient_map_image)
+
+lemma locally_connected_space_euclideanreal: "locally_connected_space euclideanreal"
+  by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_space_euclideanreal)
+
+lemma locally_connected_is_realinterval:
+   "is_interval S \<Longrightarrow> locally_connected_space(subtopology euclideanreal S)"
+  by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_is_realinterval)
+
+lemma locally_connected_real_interval:
+    "locally_connected_space (subtopology euclideanreal{a..b})"
+    "locally_connected_space (subtopology euclideanreal{a<..<b})"
+  using connected_Icc is_interval_connected_1 locally_connected_is_realinterval by auto
+
+lemma locally_connected_space_discrete_topology:
+   "locally_connected_space (discrete_topology U)"
+  by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_space_discrete_topology)
+
+lemma locally_path_connected_imp_locally_connected_at:
+   "locally_path_connected_at x X \<Longrightarrow> locally_connected_at x X"
+  by (simp add: locally_connected_at_def locally_path_connected_at_def neighbourhood_base_at_mono path_connectedin_imp_connectedin)
+
+lemma weakly_locally_path_connected_imp_weakly_locally_connected_at:
+   "weakly_locally_path_connected_at x X
+             \<Longrightarrow> weakly_locally_connected_at x X"
+  by (simp add: neighbourhood_base_at_mono path_connectedin_imp_connectedin weakly_locally_connected_at_def weakly_locally_path_connected_at_def)
+
+
+lemma interior_of_locally_connected_subspace_component:
+  assumes X: "locally_connected_space X"
+    and C: "C \<in> connected_components_of (subtopology X S)"
+  shows "X interior_of C = C \<inter> X interior_of S"
+proof -
+  obtain Csub: "C \<subseteq> topspace X" "C \<subseteq> S"
+    by (meson C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology)
+  show ?thesis
+  proof
+    show "X interior_of C \<subseteq> C \<inter> X interior_of S"
+      by (simp add: Csub interior_of_mono interior_of_subset)
+    have eq: "X interior_of S = \<Union> (connected_components_of (subtopology X (X interior_of S)))"
+      by (metis Union_connected_components_of interior_of_subset_topspace topspace_subtopology_subset)
+    moreover have "C \<inter> D \<subseteq> X interior_of C"
+      if "D \<in> connected_components_of (subtopology X (X interior_of S))" for D
+    proof (cases "C \<inter> D = {}")
+      case False
+      have "D \<subseteq> X interior_of C"
+      proof (rule interior_of_maximal)
+        have "connectedin (subtopology X S) D"
+          by (meson connectedin_connected_components_of connectedin_subtopology interior_of_subset subset_trans that)
+        then show "D \<subseteq> C"
+          by (meson C False connected_components_of_maximal disjnt_def)
+        show "openin X D"
+          using X locally_connected_space_open_connected_components openin_interior_of that by blast
+      qed
+      then show ?thesis 
+        by blast
+    qed auto
+    ultimately show "C \<inter> X interior_of S \<subseteq> X interior_of C"
+      by blast
+  qed
+qed
+
+
+lemma frontier_of_locally_connected_subspace_component:
+  assumes X: "locally_connected_space X" and "closedin X S" 
+    and C: "C \<in> connected_components_of (subtopology X S)"
+  shows "X frontier_of C = C \<inter> X frontier_of S"
+proof -
+  obtain Csub: "C \<subseteq> topspace X" "C \<subseteq> S"
+    by (meson C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology)
+  then have "X closure_of C - X interior_of C = C \<inter> X closure_of S - C \<inter> X interior_of S"
+    using assms
+    apply (simp add: closure_of_closedin flip: interior_of_locally_connected_subspace_component)
+    by (metis closedin_connected_components_of closedin_trans_full closure_of_eq inf.orderE)
+  then show ?thesis
+    by (simp add: Diff_Int_distrib frontier_of_def)
+qed
+
+(*Similar proof to locally_connected_space_prod_topology*)
+lemma locally_connected_space_prod_topology:
+   "locally_connected_space (prod_topology X Y) \<longleftrightarrow>
+      topspace (prod_topology X Y) = {} \<or>
+      locally_connected_space X \<and> locally_connected_space Y" (is "?lhs=?rhs")
+proof (cases "topspace(prod_topology X Y) = {}")
+  case True
+  then show ?thesis
+    using locally_connected_space_iff_weak by force
+next
+  case False
+  then have ne: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
+    by simp_all
+  show ?thesis
+  proof
+    assume ?lhs then show ?rhs
+      by (metis locally_connected_space_quotient_map_image ne quotient_map_fst quotient_map_snd)
+  next
+    assume ?rhs
+    with False have X: "locally_connected_space X" and Y: "locally_connected_space Y"
+      by auto
+    show ?lhs
+      unfolding locally_connected_space_def neighbourhood_base_of
+    proof clarify
+      fix UV x y
+      assume UV: "openin (prod_topology X Y) UV" and "(x,y) \<in> UV"
+
+     obtain A B where W12: "openin X A \<and> openin Y B \<and> x \<in> A \<and> y \<in> B \<and> A \<times> B \<subseteq> UV"
+        using X Y by (metis UV \<open>(x,y) \<in> UV\<close> openin_prod_topology_alt)
+      then obtain C D K L
+        where "openin X C" "connectedin X K" "x \<in> C" "C \<subseteq> K" "K \<subseteq> A"
+          "openin Y D" "connectedin Y L" "y \<in> D" "D \<subseteq> L" "L \<subseteq> B"
+        by (metis X Y locally_connected_space)
+      with W12 \<open>openin X C\<close> \<open>openin Y D\<close>
+      show "\<exists>U V. openin (prod_topology X Y) U \<and> connectedin (prod_topology X Y) V \<and> (x, y) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> UV"
+        apply (rule_tac x="C \<times> D" in exI)
+        apply (rule_tac x="K \<times> L" in exI)
+        apply (auto simp: openin_prod_Times_iff connectedin_Times)
+        done
+    qed
+  qed
+qed
+
+(*Same proof as locally_path_connected_space_product_topology*)
+lemma locally_connected_space_product_topology:
+   "locally_connected_space(product_topology X I) \<longleftrightarrow>
+        topspace(product_topology X I) = {} \<or>
+        finite {i. i \<in> I \<and> ~connected_space(X i)} \<and>
+        (\<forall>i \<in> I. locally_connected_space(X i))"
+    (is "?lhs \<longleftrightarrow> ?empty \<or> ?rhs")
+proof (cases ?empty)
+  case True
+  then show ?thesis
+    by (simp add: locally_connected_space_def neighbourhood_base_of openin_closedin_eq)
+next
+  case False
+  then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+    by auto
+  have ?rhs if L: ?lhs
+  proof -
+    obtain U C where U: "openin (product_topology X I) U"
+      and V: "connectedin (product_topology X I) C"
+      and "z \<in> U" "U \<subseteq> C" and Csub: "C \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+      using L apply (clarsimp simp add: locally_connected_space_def neighbourhood_base_of)
+      by (metis openin_topspace topspace_product_topology z)
+    then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}"
+      and XV: "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (V i)" and "z \<in> Pi\<^sub>E I V" and subU: "Pi\<^sub>E I V \<subseteq> U"
+      by (force simp: openin_product_topology_alt)
+    show ?thesis
+    proof (intro conjI ballI)
+      have "connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
+      proof -
+        have pc: "connectedin (X i) ((\<lambda>x. x i) ` C)"
+          apply (rule connectedin_continuous_map_image [OF _ V])
+          by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>)
+        moreover have "((\<lambda>x. x i) ` C) = topspace (X i)"
+        proof
+          show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)"
+            by (simp add: pc connectedin_subset_topspace)
+          have "V i \<subseteq> (\<lambda>x. x i) ` (\<Pi>\<^sub>E i\<in>I. V i)"
+            by (metis \<open>z \<in> Pi\<^sub>E I V\<close> empty_iff image_projection_PiE order_refl that(1))
+          also have "\<dots> \<subseteq> (\<lambda>x. x i) ` U"
+            using subU by blast
+          finally show "topspace (X i) \<subseteq> (\<lambda>x. x i) ` C"
+            using \<open>U \<subseteq> C\<close> that by blast
+        qed
+        ultimately show ?thesis
+          by (simp add: connectedin_topspace)
+      qed
+      then have "{i \<in> I. \<not> connected_space (X i)} \<subseteq> {i \<in> I. V i \<noteq> topspace (X i)}"
+        by blast
+      with finV show "finite {i \<in> I. \<not> connected_space (X i)}"
+        using finite_subset by blast
+    next
+      show "locally_connected_space (X i)" if "i \<in> I" for i
+        by (meson False L locally_connected_space_quotient_map_image quotient_map_product_projection that)
+    qed
+  qed
+  moreover have ?lhs if R: ?rhs
+  proof (clarsimp simp add: locally_connected_space_def neighbourhood_base_of)
+    fix F z
+    assume "openin (product_topology X I) F" and "z \<in> F"
+    then obtain W where finW: "finite {i \<in> I. W i \<noteq> topspace (X i)}"
+            and opeW: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (W i)" and "z \<in> Pi\<^sub>E I W" "Pi\<^sub>E I W \<subseteq> F"
+      by (auto simp: openin_product_topology_alt)
+    have "\<forall>i \<in> I. \<exists>U C. openin (X i) U \<and> connectedin (X i) C \<and> z i \<in> U \<and> U \<subseteq> C \<and> C \<subseteq> W i \<and>
+                        (W i = topspace (X i) \<and>
+                         connected_space (X i) \<longrightarrow> U = topspace (X i) \<and> C = topspace (X i))"
+          (is "\<forall>i \<in> I. ?\<Phi> i")
+    proof
+      fix i assume "i \<in> I"
+      have "locally_connected_space (X i)"
+        by (simp add: R \<open>i \<in> I\<close>)
+      moreover have "openin (X i) (W i) " "z i \<in> W i"
+        using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto
+      ultimately obtain U C where UC: "openin (X i) U" "connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i"
+        using \<open>i \<in> I\<close> by (force simp: locally_connected_space_def neighbourhood_base_of)
+      show "?\<Phi> i"
+      proof (cases "W i = topspace (X i) \<and> connected_space(X i)")
+        case True
+        then show ?thesis
+          using \<open>z i \<in> W i\<close> connectedin_topspace by blast
+      next
+        case False
+        then show ?thesis
+          by (meson UC)
+      qed
+    qed
+    then obtain U C where
+      *: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i) \<and> connectedin (X i) (C i) \<and> z i \<in> (U i) \<and> (U i) \<subseteq> (C i) \<and> (C i) \<subseteq> W i \<and>
+                        (W i = topspace (X i) \<and> connected_space (X i)
+                         \<longrightarrow> (U i) = topspace (X i) \<and> (C i) = topspace (X i))"
+      by metis
+    let ?A = "{i \<in> I. \<not> connected_space (X i)} \<union> {i \<in> I. W i \<noteq> topspace (X i)}"
+    have "{i \<in> I. U i \<noteq> topspace (X i)} \<subseteq> ?A"
+      by (clarsimp simp add: "*")
+    moreover have "finite ?A"
+      by (simp add: that finW)
+    ultimately have "finite {i \<in> I. U i \<noteq> topspace (X i)}"
+      using finite_subset by auto
+    then have "openin (product_topology X I) (Pi\<^sub>E I U)"
+      using * by (simp add: openin_PiE_gen)
+    then show "\<exists>U. openin (product_topology X I) U \<and>
+            (\<exists>V. connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
+      apply (rule_tac x="PiE I U" in exI, simp)
+      apply (rule_tac x="PiE I C" in exI)
+      using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> *
+      apply (simp add: connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans)
+      done
+  qed
+  ultimately show ?thesis
+    using False by blast
+qed
+
+lemma locally_connected_space_sum_topology:
+   "locally_connected_space(sum_topology X I) \<longleftrightarrow>
+    (\<forall>i \<in> I. locally_connected_space (X i))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (smt (verit) homeomorphic_locally_connected_space locally_connected_space_open_subset topological_property_of_sum_component)
+next
+  assume R: ?rhs
+  show ?lhs
+  proof (clarsimp simp add: locally_connected_space_def neighbourhood_base_of forall_openin_sum_topology imp_conjL)
+    fix W i x
+    assume ope: "\<forall>i\<in>I. openin (X i) (W i)" 
+      and "i \<in> I" and "x \<in> W i"
+    then obtain U V where U: "openin (X i) U" and V: "connectedin (X i) V" 
+           and "x \<in> U" "U \<subseteq> V" "V \<subseteq> W i"
+      by (metis R \<open>i \<in> I\<close> \<open>x \<in> W i\<close> locally_connected_space)
+    show "\<exists>U. openin (sum_topology X I) U \<and> (\<exists>V. connectedin (sum_topology X I) V \<and> (i,x) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> Sigma I W)"
+    proof (intro exI conjI)
+      show "openin (sum_topology X I) (Pair i ` U)"
+        by (meson U \<open>i \<in> I\<close> open_map_component_injection open_map_def)
+      show "connectedin (sum_topology X I) (Pair i ` V)"
+        by (meson V \<open>i \<in> I\<close> continuous_map_component_injection connectedin_continuous_map_image)
+      show "Pair i ` V \<subseteq> Sigma I W"
+        using \<open>V \<subseteq> W i\<close> \<open>i \<in> I\<close> by force
+    qed (use \<open>x \<in> U\<close> \<open>U \<subseteq> V\<close> in auto)
+  qed
+qed
+
+
 end
diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Thu May 11 22:12:43 2023 +0200
+++ b/src/HOL/Analysis/Product_Topology.thy	Mon May 15 17:12:18 2023 +0100
@@ -576,5 +576,68 @@
     by (metis prod.collapse)
 qed
 
+proposition connected_space_prod_topology:
+   "connected_space(prod_topology X Y) \<longleftrightarrow>
+    topspace(prod_topology X Y) = {} \<or> connected_space X \<and> connected_space Y" (is "?lhs=?rhs")
+proof (cases "topspace(prod_topology X Y) = {}")
+  case True
+  then show ?thesis
+    using connected_space_topspace_empty by blast
+next
+  case False
+  then have nonempty: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
+    by force+
+  show ?thesis 
+  proof
+    assume ?lhs
+    then show ?rhs
+      by (meson connected_space_quotient_map_image nonempty quotient_map_fst quotient_map_snd)
+  next
+    assume ?rhs
+    then have conX: "connected_space X" and conY: "connected_space Y"
+      using False by blast+
+    have False
+      if "openin (prod_topology X Y) U" and "openin (prod_topology X Y) V"
+        and UV: "topspace X \<times> topspace Y \<subseteq> U \<union> V" "U \<inter> V = {}" 
+        and "U \<noteq> {}" and "V \<noteq> {}"
+      for U V
+    proof -
+      have Usub: "U \<subseteq> topspace X \<times> topspace Y" and Vsub: "V \<subseteq> topspace X \<times> topspace Y"
+        using that by (metis openin_subset topspace_prod_topology)+
+      obtain a b where ab: "(a,b) \<in> U" and a: "a \<in> topspace X" and b: "b \<in> topspace Y"
+        using \<open>U \<noteq> {}\<close> Usub by auto
+      have "\<not> topspace X \<times> topspace Y \<subseteq> U"
+        using Usub Vsub \<open>U \<inter> V = {}\<close> \<open>V \<noteq> {}\<close> by auto
+      then obtain x y where x: "x \<in> topspace X" and y: "y \<in> topspace Y" and "(x,y) \<notin> U"
+        by blast
+      have oX: "openin X {x \<in> topspace X. (x,y) \<in> U}" "openin X {x \<in> topspace X. (x,y) \<in> V}"
+       and oY: "openin Y {y \<in> topspace Y. (a,y) \<in> U}" "openin Y {y \<in> topspace Y. (a,y) \<in> V}"
+        by (force intro: openin_continuous_map_preimage [where Y = "prod_topology X Y"] 
+            simp: that continuous_map_pairwise o_def x y a)+
+      have 1: "topspace Y \<subseteq> {y \<in> topspace Y. (a,y) \<in> U} \<union> {y \<in> topspace Y. (a,y) \<in> V}"
+        using a that(3) by auto
+      have 2: "{y \<in> topspace Y. (a,y) \<in> U} \<inter> {y \<in> topspace Y. (a,y) \<in> V} = {}"
+        using that(4) by auto
+      have 3: "{y \<in> topspace Y. (a,y) \<in> U} \<noteq> {}"
+        using ab b by auto
+      have 4: "{y \<in> topspace Y. (a,y) \<in> V} \<noteq> {}"
+      proof -
+        show ?thesis
+          using connected_spaceD [OF conX oX] UV \<open>(x,y) \<notin> U\<close> a x y
+                disjoint_iff_not_equal by blast
+      qed
+      show ?thesis
+        using connected_spaceD [OF conY oY 1 2 3 4] by auto
+    qed
+    then show ?lhs
+      unfolding connected_space_def topspace_prod_topology by blast 
+  qed
+qed
+
+lemma connectedin_Times:
+   "connectedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow>
+        S = {} \<or> T = {} \<or> connectedin X S \<and> connectedin Y T"
+  by (force simp: connectedin_def subtopology_Times connected_space_prod_topology)
+
 end
 
diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu May 11 22:12:43 2023 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Mon May 15 17:12:18 2023 +0100
@@ -882,6 +882,11 @@
     convex_rel_interior_closure[of S] assms
   by auto
 
+lemma open_subset_closure_of_interval:
+  assumes "open U" "is_interval S"
+  shows "U \<subseteq> closure S \<longleftrightarrow> U \<subseteq> interior S"
+  by (metis assms convex_interior_closure is_interval_convex open_subset_interior)
+
 lemma closure_eq_rel_interior_eq:
   fixes S1 S2 :: "'n::euclidean_space set"
   assumes "convex S1"
diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Sum_Topology.thy
--- a/src/HOL/Analysis/Sum_Topology.thy	Thu May 11 22:12:43 2023 +0200
+++ b/src/HOL/Analysis/Sum_Topology.thy	Mon May 15 17:12:18 2023 +0100
@@ -143,4 +143,20 @@
   by (metis injective_open_imp_embedding_map continuous_map_component_injection
             open_map_component_injection inj_onI prod.inject)
 
+lemma topological_property_of_sum_component:
+  assumes major: "P (sum_topology X I)"
+    and minor: "\<And>X S. \<lbrakk>P X; closedin X S; openin X S\<rbrakk> \<Longrightarrow> P(subtopology X S)"
+    and PQ:  "\<And>X Y. X homeomorphic_space Y \<Longrightarrow> (P X \<longleftrightarrow> Q Y)"
+  shows "(\<forall>i \<in> I. Q(X i))"
+proof -
+  have "Q(X i)" if "i \<in> I" for i
+  proof -
+    have "P(subtopology (sum_topology X I) (Pair i ` topspace (X i)))"
+      by (meson closed_map_component_injection closed_map_def closedin_topspace major minor open_map_component_injection open_map_def openin_topspace that)
+    then show ?thesis
+      by (metis PQ embedding_map_component_injection embedding_map_imp_homeomorphic_space homeomorphic_space_sym that)
+  qed
+  then show ?thesis by metis
+qed
+
 end