# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1683037059 -3600
# Node ID 7f240b0dabd9666cd69e44400bc97775c83bd803
# Parent  01c88cf514fcfc704246cb164d27c62a551a5dc1
More new theorems, and a necessary correction

diff -r 01c88cf514fc -r 7f240b0dabd9 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue May 02 15:17:39 2023 +0100
@@ -297,6 +297,10 @@
   unfolding closedin_def topspace_subtopology
   by (auto simp: openin_subtopology)
 
+lemma closedin_relative_to:
+   "(closedin X relative_to S) = closedin (subtopology X S)"
+  by (force simp: relative_to_def closedin_subtopology)
+
 lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
   unfolding openin_subtopology
   by auto (metis IntD1 in_mono openin_subset)
@@ -1879,6 +1883,250 @@
     by (metis \<open>closedin X T\<close> closed_map_def closedin_subtopology f)
 qed
 
+lemma closed_map_closure_of_image:
+   "closed_map X Y f \<longleftrightarrow>
+        f ` topspace X \<subseteq> topspace Y \<and>
+        (\<forall>S. S \<subseteq> topspace X \<longrightarrow> Y closure_of (f ` S) \<subseteq> image f (X closure_of S))" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (simp add: closed_map_def closed_map_imp_subset_topspace closure_of_minimal closure_of_subset image_mono)
+next
+  assume ?rhs
+  then show ?lhs
+    by (metis closed_map_def closed_map_into_discrete_topology closure_of_eq 
+        closure_of_subset_eq topspace_discrete_topology)
+qed
+
+lemma open_map_interior_of_image_subset:
+  "open_map X Y f \<longleftrightarrow> (\<forall>S. image f (X interior_of S) \<subseteq> Y interior_of (f ` S))"
+  by (metis image_mono interior_of_eq interior_of_maximal interior_of_subset open_map_def openin_interior_of subset_antisym)
+
+lemma open_map_interior_of_image_subset_alt:
+  "open_map X Y f \<longleftrightarrow> (\<forall>S\<subseteq>topspace X. f ` (X interior_of S) \<subseteq> Y interior_of f ` S)"
+  by (metis interior_of_eq open_map_def open_map_interior_of_image_subset openin_subset subset_interior_of_eq)
+
+lemma open_map_interior_of_image_subset_gen:
+  "open_map X Y f \<longleftrightarrow>
+       (f ` topspace X \<subseteq> topspace Y \<and> (\<forall>S. f ` (X interior_of S) \<subseteq> Y interior_of f ` S))"
+  by (meson open_map_imp_subset_topspace open_map_interior_of_image_subset)
+
+lemma open_map_preimage_neighbourhood:
+   "open_map X Y f \<longleftrightarrow>
+    (f ` topspace X \<subseteq> topspace Y \<and>
+     (\<forall>U T. closedin X U \<and> T \<subseteq> topspace Y \<and>
+            {x \<in> topspace X. f x \<in> T} \<subseteq> U \<longrightarrow>
+            (\<exists>V. closedin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U)))" (is "?lhs=?rhs")
+proof
+  assume L: ?lhs
+  show ?rhs
+  proof (intro conjI strip)
+    show "f ` topspace X \<subseteq> topspace Y"
+      by (simp add: \<open>open_map X Y f\<close> open_map_imp_subset_topspace)
+  next
+    fix U T
+    assume UT: "closedin X U \<and> T \<subseteq> topspace Y \<and> {x \<in> topspace X. f x \<in> T} \<subseteq> U"
+    have "closedin Y (topspace Y - f ` (topspace X - U))"
+      by (meson UT L open_map_def openin_closedin_eq openin_diff openin_topspace)
+    with UT
+    show "\<exists>V. closedin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U"
+      using image_iff by auto
+  qed
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding open_map_def
+  proof (intro strip)
+    fix U assume "openin X U"
+    have "{x \<in> topspace X. f x \<in> topspace Y - f ` U} \<subseteq> topspace X - U"
+      by blast
+    then obtain V where V: "closedin Y V" 
+      and sub: "topspace Y - f ` U \<subseteq> V" "{x \<in> topspace X. f x \<in> V} \<subseteq> topspace X - U"
+      using R \<open>openin X U\<close> by (meson Diff_subset openin_closedin_eq) 
+    then have "f ` U \<subseteq> topspace Y - V"
+      using R \<open>openin X U\<close> openin_subset by fastforce
+    with sub have "f ` U = topspace Y - V"
+      by auto
+    then show "openin Y (f ` U)"
+      using V(1) by auto
+  qed
+qed
+
+
+lemma closed_map_preimage_neighbourhood:
+   "closed_map X Y f \<longleftrightarrow>
+        image f (topspace X) \<subseteq> topspace Y \<and>
+        (\<forall>U T. openin X U \<and> T \<subseteq> topspace Y \<and>
+              {x \<in> topspace X. f x \<in> T} \<subseteq> U
+              \<longrightarrow> (\<exists>V. openin Y V \<and> T \<subseteq> V \<and>
+                      {x \<in> topspace X. f x \<in> V} \<subseteq> U))" (is "?lhs=?rhs")
+proof
+  assume L: ?lhs
+  show ?rhs
+  proof (intro conjI strip)
+    show "f ` topspace X \<subseteq> topspace Y"
+      by (simp add: L closed_map_imp_subset_topspace)
+  next
+    fix U T
+    assume UT: "openin X U \<and> T \<subseteq> topspace Y \<and> {x \<in> topspace X. f x \<in> T} \<subseteq> U"
+    then have "openin Y (topspace Y - f ` (topspace X - U))"
+      by (meson L closed_map_def closedin_def closedin_diff closedin_topspace)
+    then show "\<exists>V. openin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U"
+      using UT image_iff by auto
+  qed
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding closed_map_def
+  proof (intro strip)
+    fix U assume "closedin X U"
+    have "{x \<in> topspace X. f x \<in> topspace Y - f ` U} \<subseteq> topspace X - U"
+      by blast
+    then obtain V where V: "openin Y V" 
+      and sub: "topspace Y - f ` U \<subseteq> V" "{x \<in> topspace X. f x \<in> V} \<subseteq> topspace X - U"
+      using R Diff_subset \<open>closedin X U\<close> unfolding closedin_def
+      by (smt (verit, ccfv_threshold) Collect_mem_eq Collect_mono_iff)
+    then have "f ` U \<subseteq> topspace Y - V"
+      using R \<open>closedin X U\<close> closedin_subset by fastforce
+    with sub have "f ` U = topspace Y - V"
+      by auto
+    with V show "closedin Y (f ` U)"
+      by auto
+  qed
+qed
+
+lemma closed_map_fibre_neighbourhood:
+  "closed_map X Y f \<longleftrightarrow>
+     f ` (topspace X) \<subseteq> topspace Y \<and>
+     (\<forall>U y. openin X U \<and> y \<in> topspace Y \<and> {x \<in> topspace X. f x = y} \<subseteq> U
+     \<longrightarrow> (\<exists>V. openin Y V \<and> y \<in> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U))"
+  unfolding closed_map_preimage_neighbourhood
+proof (intro conj_cong refl all_cong1)
+  fix U
+  assume "f ` topspace X \<subseteq> topspace Y"
+  show "(\<forall>T. openin X U \<and> T \<subseteq> topspace Y \<and> {x \<in> topspace X. f x \<in> T} \<subseteq> U 
+         \<longrightarrow> (\<exists>V. openin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U))
+      = (\<forall>y. openin X U \<and> y \<in> topspace Y \<and> {x \<in> topspace X. f x = y} \<subseteq> U 
+         \<longrightarrow> (\<exists>V. openin Y V \<and> y \<in> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U))" 
+    (is "(\<forall>T. ?P T) \<longleftrightarrow> (\<forall>y. ?Q y)")
+  proof
+    assume L [rule_format]: "\<forall>T. ?P T"
+    show "\<forall>y. ?Q y"
+    proof
+      fix y show "?Q y"
+        using L [of "{y}"] by blast
+    qed
+  next
+    assume R: "\<forall>y. ?Q y"
+    show "\<forall>T. ?P T"
+    proof (cases "openin X U")
+      case True
+      note [[unify_search_bound=3]]
+      obtain V where V: "\<And>y. \<lbrakk>y \<in> topspace Y; {x \<in> topspace X. f x = y} \<subseteq> U\<rbrakk> \<Longrightarrow>
+                       openin Y (V y) \<and> y \<in> V y \<and> {x \<in> topspace X. f x \<in> V y} \<subseteq> U"
+        using R by (simp add: True) meson
+      show ?thesis
+      proof clarify
+        fix T
+        assume "openin X U" and "T \<subseteq> topspace Y" and "{x \<in> topspace X. f x \<in> T} \<subseteq> U"
+        with V show "\<exists>V. openin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U"
+          by (rule_tac x="\<Union>y\<in>T. V y" in exI) fastforce
+      qed
+    qed auto
+  qed
+qed
+
+lemma open_map_in_subtopology:
+   "openin Y S
+        \<Longrightarrow> (open_map X (subtopology Y S) f \<longleftrightarrow> open_map X Y f \<and> f ` (topspace X) \<subseteq> S)"
+  by (metis le_inf_iff open_map_def open_map_imp_subset_topspace open_map_into_subtopology openin_trans_full topspace_subtopology)
+
+lemma open_map_from_open_subtopology:
+   "\<lbrakk>openin Y S; open_map X (subtopology Y S) f\<rbrakk> \<Longrightarrow> open_map X Y f"
+  using open_map_in_subtopology by blast
+
+lemma closed_map_in_subtopology:
+   "closedin Y S
+        \<Longrightarrow> closed_map X (subtopology Y S) f \<longleftrightarrow> (closed_map X Y f \<and> f ` topspace X \<subseteq> S)"
+  by (metis closed_map_def closed_map_imp_subset_topspace closed_map_into_subtopology 
+        closedin_closed_subtopology closedin_subset topspace_subtopology_subset)
+
+lemma closed_map_from_closed_subtopology:
+   "\<lbrakk>closedin Y S; closed_map X (subtopology Y S) f\<rbrakk> \<Longrightarrow> closed_map X Y f"
+  using closed_map_in_subtopology by blast
+
+lemma closed_map_from_composition_left:
+  assumes cmf: "closed_map X Z (g \<circ> f)" and contf: "continuous_map X Y f" and fim: "f ` topspace X = topspace Y"
+  shows "closed_map Y Z g"
+  unfolding closed_map_def
+proof (intro strip)
+  fix U assume "closedin Y U"
+  then have "closedin X {x \<in> topspace X. f x \<in> U}"
+    using contf closedin_continuous_map_preimage by blast
+  then have "closedin Z ((g \<circ> f) ` {x \<in> topspace X. f x \<in> U})"
+    using cmf closed_map_def by blast
+  moreover 
+  have "\<And>y. y \<in> U \<Longrightarrow> \<exists>x \<in> topspace X. f x \<in> U \<and> g y = g (f x)"
+    by (smt (verit, ccfv_SIG) \<open>closedin Y U\<close> closedin_subset fim image_iff subsetD)
+  then have "(g \<circ> f) ` {x \<in> topspace X. f x \<in> U} = g`U" by auto
+  ultimately show "closedin Z (g ` U)"
+    by metis
+qed
+
+text \<open>identical proof as the above\<close>
+lemma open_map_from_composition_left:
+  assumes cmf: "open_map X Z (g \<circ> f)" and contf: "continuous_map X Y f" and fim: "f ` topspace X = topspace Y"
+  shows "open_map Y Z g"
+  unfolding open_map_def
+proof (intro strip)
+  fix U assume "openin Y U"
+  then have "openin X {x \<in> topspace X. f x \<in> U}"
+    using contf openin_continuous_map_preimage by blast
+  then have "openin Z ((g \<circ> f) ` {x \<in> topspace X. f x \<in> U})"
+    using cmf open_map_def by blast
+  moreover 
+  have "\<And>y. y \<in> U \<Longrightarrow> \<exists>x \<in> topspace X. f x \<in> U \<and> g y = g (f x)"
+    by (smt (verit, ccfv_SIG) \<open>openin Y U\<close> openin_subset fim image_iff subsetD)
+  then have "(g \<circ> f) ` {x \<in> topspace X. f x \<in> U} = g`U" by auto
+  ultimately show "openin Z (g ` U)"
+    by metis
+qed
+
+lemma closed_map_from_composition_right:
+  assumes cmf: "closed_map X Z (g \<circ> f)" "f ` topspace X \<subseteq> topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)"
+  shows "closed_map X Y f"
+  unfolding closed_map_def
+proof (intro strip)
+  fix C assume "closedin X C"
+  have "\<And>y c. \<lbrakk>y \<in> topspace Y; g y = g (f c); c \<in> C\<rbrakk> \<Longrightarrow> y \<in> f ` C"
+    using \<open>closedin X C\<close> assms closedin_subset inj_onD by fastforce
+  then
+  have "f ` C = {x \<in> topspace Y. g x \<in> (g \<circ> f) ` C}"
+    using \<open>closedin X C\<close> assms(2) closedin_subset by fastforce
+  moreover have "closedin Z ((g \<circ> f) ` C)"
+    using \<open>closedin X C\<close> cmf closed_map_def by blast
+  ultimately show "closedin Y (f ` C)"
+    using assms(3) closedin_continuous_map_preimage by fastforce
+qed
+
+text \<open>identical proof as the above\<close>
+lemma open_map_from_composition_right:
+  assumes "open_map X Z (g \<circ> f)" "f ` topspace X \<subseteq> topspace Y" "continuous_map Y Z g" "inj_on g (topspace Y)"
+  shows "open_map X Y f"
+  unfolding open_map_def
+proof (intro strip)
+  fix C assume "openin X C"
+  have "\<And>y c. \<lbrakk>y \<in> topspace Y; g y = g (f c); c \<in> C\<rbrakk> \<Longrightarrow> y \<in> f ` C"
+    using \<open>openin X C\<close> assms openin_subset inj_onD by fastforce
+  then
+  have "f ` C = {x \<in> topspace Y. g x \<in> (g \<circ> f) ` C}"
+    using \<open>openin X C\<close> assms(2) openin_subset by fastforce
+  moreover have "openin Z ((g \<circ> f) ` C)"
+    using \<open>openin X C\<close> assms(1) open_map_def by blast
+  ultimately show "openin Y (f ` C)"
+    using assms(3) openin_continuous_map_preimage by fastforce
+qed
+
 subsection\<open>Quotient maps\<close>
                                       
 definition quotient_map where
@@ -2163,6 +2411,84 @@
   qed
 qed
 
+lemma quotient_map_saturated_closed:
+     "quotient_map X Y f \<longleftrightarrow>
+        continuous_map X Y f \<and> f ` (topspace X) = topspace Y \<and>
+        (\<forall>U. closedin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U \<longrightarrow> closedin Y (f ` U))"
+     (is "?lhs = ?rhs")
+proof
+  assume L: ?lhs
+  then obtain fim: "f ` topspace X = topspace Y"
+    and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> closedin Y U = closedin X {x \<in> topspace X. f x \<in> U}"
+    by (simp add: quotient_map_closedin)
+  show ?rhs
+  proof (intro conjI allI impI)
+    show "continuous_map X Y f"
+      by (simp add: L quotient_imp_continuous_map)
+    show "f ` topspace X = topspace Y"
+      by (simp add: fim)
+  next
+    fix U :: "'a set"
+    assume U: "closedin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U"
+    then have sub:  "f ` U \<subseteq> topspace Y" and eq: "{x \<in> topspace X. f x \<in> f ` U} = U"
+      using fim closedin_subset by fastforce+
+    show "closedin Y (f ` U)"
+      by (simp add: sub Y eq U)
+  qed
+next
+  assume ?rhs
+  then obtain YX: "\<And>U. closedin Y U \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> U}"
+    and fim: "f ` topspace X = topspace Y"
+    and XY: "\<And>U. \<lbrakk>closedin X U; {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U\<rbrakk> \<Longrightarrow> closedin Y (f ` U)"
+    by (simp add: continuous_map_closedin)
+  show ?lhs
+  proof (simp add: quotient_map_closedin fim, intro allI impI iffI)
+    fix U :: "'b set"
+    assume "U \<subseteq> topspace Y" and X: "closedin X {x \<in> topspace X. f x \<in> U}"
+    have feq: "f ` {x \<in> topspace X. f x \<in> U} = U"
+      using \<open>U \<subseteq> topspace Y\<close> fim by auto
+    show "closedin Y U"
+      using XY [OF X] by (simp add: feq)
+  next
+    fix U :: "'b set"
+    assume "U \<subseteq> topspace Y" and Y: "closedin Y U"
+    show "closedin X {x \<in> topspace X. f x \<in> U}"
+      by (metis YX [OF Y])
+  qed
+qed
+
+lemma quotient_map_onto_image:
+  assumes "f ` topspace X \<subseteq> topspace Y" and U: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
+  shows "quotient_map X (subtopology Y (f ` topspace X)) f"
+  unfolding quotient_map_def topspace_subtopology
+proof (intro conjI strip)
+  fix U
+  assume "U \<subseteq> topspace Y \<inter> f ` topspace X"
+  with U have "openin X {x \<in> topspace X. f x \<in> U} \<Longrightarrow> \<exists>x. openin Y x \<and> U = f ` topspace X \<inter> x"
+    by fastforce
+  moreover have "\<exists>x. openin Y x \<and> U = f ` topspace X \<inter> x \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
+    by (metis (mono_tags, lifting) Collect_cong IntE IntI U image_eqI openin_subset)
+  ultimately show "openin X {x \<in> topspace X. f x \<in> U} = openin (subtopology Y (f ` topspace X)) U"
+    by (force simp: openin_subtopology_alt image_iff)
+qed (use assms in auto)
+
+lemma quotient_map_lift_exists:
+  assumes f: "quotient_map X Y f" and h: "continuous_map X Z h" 
+    and "\<And>x y. \<lbrakk>x \<in> topspace X; y \<in> topspace X; f x = f y\<rbrakk> \<Longrightarrow> h x = h y"
+  obtains g where "continuous_map Y Z g" "g ` topspace Y = h ` topspace X"
+                  "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = h x"
+proof -
+  obtain g where g: "\<And>x. x \<in> topspace X \<Longrightarrow> h x = g(f x)"
+    using function_factors_left_gen[of "\<lambda>x. x \<in> topspace X" f h] assms by blast
+  show ?thesis
+  proof
+    show "g ` topspace Y = h ` topspace X"
+      using f g by (force dest!: quotient_imp_surjective_map)
+    show "continuous_map Y Z g"
+      by (smt (verit)  f g h continuous_compose_quotient_map_eq continuous_map_eq o_def)
+  qed (simp add: g)
+qed
+
 subsection\<open> Separated Sets\<close>
 
 definition separatedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
@@ -2257,6 +2583,11 @@
   unfolding openin_closedin_eq topspace_subtopology separation_closedin_Un_gen disjnt_def
   by (auto simp: Diff_triv Int_commute Un_Diff inf_absorb1 topspace_def)
 
+lemma separatedin_full:
+   "S \<union> T = topspace X
+   \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T \<and> closedin X S \<and> openin X S \<and> closedin X T \<and> openin X T"
+  by (metis separatedin_open_sets separation_closedin_Un_gen separation_openin_Un_gen subtopology_topspace)
+
 
 subsection\<open>Homeomorphisms\<close>
 text\<open>(1-way and 2-way versions may be useful in places)\<close>
@@ -2778,6 +3109,10 @@
     by (intro conj_cong arg_cong [where f=Not] ex_cong1; blast dest!: openin_subset)
 qed
 
+lemma connectedinD:
+     "\<lbrakk>connectedin X S; openin X E1; openin X E2; S \<subseteq> E1 \<union> E2; E1 \<inter> E2 \<inter> S = {}; E1 \<inter> S \<noteq> {}; E2 \<inter> S \<noteq> {}\<rbrakk> \<Longrightarrow> False"
+  by (meson connectedin)
+
 lemma connectedin_iff_connected [simp]: "connectedin euclidean S \<longleftrightarrow> connected S"
   by (simp add: connected_def connectedin)
 
@@ -3080,7 +3415,7 @@
     moreover have "connectedin (discrete_topology U) S \<longleftrightarrow> (\<exists>a. S = {a})"
     proof
       show "connectedin (discrete_topology U) S \<Longrightarrow> \<exists>a. S = {a}"
-        using False connectedin_inter_frontier_of insert_Diff by fastforce
+        using False connectedin_Int_frontier_of insert_Diff by fastforce
     qed (use True in auto)
     ultimately show ?thesis
       by auto
@@ -3568,6 +3903,10 @@
   unfolding closed_map_def
   by (auto simp: closedin_closed_subtopology embedding_map_def homeomorphic_map_closedness_eq)
 
+lemma embedding_imp_closed_map_eq:
+   "embedding_map X Y f \<Longrightarrow> (closed_map X Y f \<longleftrightarrow> closedin Y (f ` topspace X))"
+  using closed_map_def embedding_imp_closed_map by blast
+
 
 subsection\<open>Retraction and section maps\<close>
 
diff -r 01c88cf514fc -r 7f240b0dabd9 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue May 02 15:17:39 2023 +0100
@@ -1716,6 +1716,11 @@
   shows "connected S \<longleftrightarrow> convex S"
   by (metis is_interval_convex convex_connected is_interval_connected_1)
 
+lemma connected_space_iff_is_interval_1 [iff]:
+  fixes S :: "real set"
+  shows "connected_space (top_of_set S) \<longleftrightarrow> is_interval S"
+  using connectedin_topspace is_interval_connected_1 by force
+
 lemma connected_convex_1_gen:
   fixes S :: "'a :: euclidean_space set"
   assumes "DIM('a) = 1"
diff -r 01c88cf514fc -r 7f240b0dabd9 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Tue May 02 15:17:39 2023 +0100
@@ -969,9 +969,6 @@
 
 subsection\<open> Special cases and corollaries involving spheres\<close>
 
-lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
-  by (auto simp: disjnt_def)
-
 proposition extend_map_affine_to_sphere_cofinite_simple:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "compact S" "convex U" "bounded U"
diff -r 01c88cf514fc -r 7f240b0dabd9 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue May 02 15:17:39 2023 +0100
@@ -2,7 +2,7 @@
 
 theory Ordered_Euclidean_Space
 imports
-  Convex_Euclidean_Space
+  Convex_Euclidean_Space Abstract_Limits
   "HOL-Library.Product_Order"
 begin
 
@@ -157,6 +157,32 @@
   shows "((\<lambda>i. inf (X i) (Y i)) \<longlongrightarrow> inf x y) net"
    unfolding inf_min eucl_inf by (intro assms tendsto_intros)
 
+lemma tendsto_Inf:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
+  assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> l i) F"
+  shows "((\<lambda>x. Inf (f x ` K)) \<longlongrightarrow> Inf (l ` K)) F"
+  using assms
+  by (induction K rule: finite_induct) (auto simp: cInf_insert_If tendsto_inf)
+
+lemma tendsto_Sup:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
+  assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> l i) F"
+  shows "((\<lambda>x. Sup (f x ` K)) \<longlongrightarrow> Sup (l ` K)) F"
+  using assms
+  by (induction K rule: finite_induct) (auto simp: cSup_insert_If tendsto_sup)
+
+lemma continuous_map_Inf:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
+  assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x i)"
+  shows "continuous_map X euclidean (\<lambda>x. INF i\<in>K. f x i)"
+  using assms by (simp add: continuous_map_atin tendsto_Inf)
+
+lemma continuous_map_Sup:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::ordered_euclidean_space"
+  assumes "finite K" "\<And>i. i \<in> K \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x i)"
+  shows "continuous_map X euclidean (\<lambda>x. SUP i\<in>K. f x i)"
+  using assms by (simp add: continuous_map_atin tendsto_Sup)
+
 lemma tendsto_componentwise_max:
   assumes f: "(f \<longlongrightarrow> l) F" and g: "(g \<longlongrightarrow> m) F"
   shows "((\<lambda>x. (\<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)) \<longlongrightarrow> (\<Sum>i\<in>Basis. max (l \<bullet> i) (m \<bullet> i) *\<^sub>R i)) F"
@@ -167,10 +193,6 @@
   shows "((\<lambda>x. (\<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)) \<longlongrightarrow> (\<Sum>i\<in>Basis. min (l \<bullet> i) (m \<bullet> i) *\<^sub>R i)) F"
   by (intro tendsto_intros assms)
 
-lemma (in order) atLeastatMost_empty'[simp]:
-  "(\<not> a \<le> b) \<Longrightarrow> {a..b} = {}"
-  by (auto)
-
 instance real :: ordered_euclidean_space
   by standard auto
 
diff -r 01c88cf514fc -r 7f240b0dabd9 src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/Product_Topology.thy	Tue May 02 15:17:39 2023 +0100
@@ -464,6 +464,10 @@
    "homeomorphic_map (prod_topology X Y) (prod_topology Y X) (\<lambda>(x,y). (y,x))"
   using homeomorphic_map_maps homeomorphic_maps_swap by metis
 
+lemma homeomorphic_space_prod_topology_swap:
+   "(prod_topology X Y) homeomorphic_space (prod_topology Y X)"
+  using homeomorphic_map_swap homeomorphic_space by blast
+
 lemma embedding_map_graph:
    "embedding_map X (prod_topology X Y) (\<lambda>x. (x, f x)) \<longleftrightarrow> continuous_map X Y f"
     (is "?lhs = ?rhs")
@@ -472,8 +476,7 @@
   have "snd \<circ> (\<lambda>x. (x, f x)) = f"
     by force
   moreover have "continuous_map X Y (snd \<circ> (\<lambda>x. (x, f x)))"
-    using L
-    unfolding embedding_map_def
+    using L unfolding embedding_map_def
     by (meson continuous_map_in_subtopology continuous_map_snd_of homeomorphic_imp_continuous_map)
   ultimately show ?rhs
     by simp
diff -r 01c88cf514fc -r 7f240b0dabd9 src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy	Tue May 02 15:17:39 2023 +0100
@@ -380,8 +380,7 @@
 lemma Hausdorff_space_discrete_topology [simp]:
    "Hausdorff_space (discrete_topology U)"
   unfolding Hausdorff_space_def
-  apply safe
-  by (metis discrete_topology_unique_alt disjnt_empty2 disjnt_insert2 insert_iff mk_disjoint_insert topspace_discrete_topology)
+  by (metis Hausdorff_space_compact_sets Hausdorff_space_def compactin_discrete_topology equalityE openin_discrete_topology)
 
 lemma compactin_Int:
    "\<lbrakk>Hausdorff_space X; compactin X S; compactin X T\<rbrakk> \<Longrightarrow> compactin X (S \<inter> T)"
@@ -395,6 +394,10 @@
    "\<lbrakk>Hausdorff_space X; finite S\<rbrakk> \<Longrightarrow> X derived_set_of S = {}"
   using Hausdorff_imp_t1_space t1_space_derived_set_of_finite by auto
 
+lemma infinite_perfect_set:
+   "\<lbrakk>Hausdorff_space X; S \<subseteq> X derived_set_of S; S \<noteq> {}\<rbrakk> \<Longrightarrow> infinite S"
+  using derived_set_of_finite by blast
+
 lemma derived_set_of_singleton:
    "Hausdorff_space X \<Longrightarrow> X derived_set_of {x} = {}"
   by (simp add: derived_set_of_finite)
@@ -698,4 +701,47 @@
   qed
 qed
 
+lemma Hausdorff_space_closed_neighbourhood:
+   "Hausdorff_space X \<longleftrightarrow>
+    (\<forall>x \<in> topspace X. \<exists>U C. openin X U \<and> closedin X C \<and>
+                      Hausdorff_space(subtopology X C) \<and> x \<in> U \<and> U \<subseteq> C)" (is "_ = ?rhs")
+proof
+  assume R: ?rhs
+  show "Hausdorff_space X"
+    unfolding Hausdorff_space_def
+  proof clarify
+    fix x y
+    assume x: "x \<in> topspace X" and y: "y \<in> topspace X" and "x \<noteq> y"
+    obtain T C where *: "openin X T" "closedin X C" "x \<in> T" "T \<subseteq> C"
+                 and C: "Hausdorff_space (subtopology X C)"
+      by (meson R \<open>x \<in> topspace X\<close>)
+    show "\<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
+    proof (cases "y \<in> C")
+      case True
+      with * C obtain U V where U: "openin (subtopology X C) U"
+                        and V: "openin (subtopology X C) V"
+                        and "x \<in> U" "y \<in> V" "disjnt U V"
+        unfolding Hausdorff_space_def
+        by (smt (verit, best) \<open>x \<noteq> y\<close> closedin_subset subsetD topspace_subtopology_subset)
+      then obtain U' V' where UV': "U = U' \<inter> C" "openin X U'" "V = V' \<inter> C" "openin X V'"
+        by (meson openin_subtopology)
+      have "disjnt (T \<inter> U') V'"
+        using \<open>disjnt U V\<close> UV' \<open>T \<subseteq> C\<close> by (force simp: disjnt_iff)
+      with \<open>T \<subseteq> C\<close> have "disjnt (T \<inter> U') (V' \<union> (topspace X - C))"
+        unfolding disjnt_def by blast
+      moreover
+      have "openin X (T \<inter> U')"
+        by (simp add: \<open>openin X T\<close> \<open>openin X U'\<close> openin_Int)
+      moreover have "openin X (V' \<union> (topspace X - C))"
+        using \<open>closedin X C\<close> \<open>openin X V'\<close> by auto
+      ultimately show ?thesis
+        using UV' \<open>x \<in> T\<close> \<open>x \<in> U\<close> \<open>y \<in> V\<close> by blast
+    next
+      case False
+      with * y show ?thesis
+        by (force simp: closedin_def disjnt_def)
+    qed
+  qed
+qed fastforce
+    
 end
diff -r 01c88cf514fc -r 7f240b0dabd9 src/HOL/Library/Set_Idioms.thy
--- a/src/HOL/Library/Set_Idioms.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Library/Set_Idioms.thy	Tue May 02 15:17:39 2023 +0100
@@ -557,4 +557,162 @@
     by blast
 qed
 
+lemma countable_union_of_empty [simp]: "(countable union_of P) {}"
+  by (simp add: union_of_empty)
+
+lemma countable_intersection_of_empty [simp]: "(countable intersection_of P) UNIV"
+  by (simp add: intersection_of_empty)
+
+lemma countable_union_of_inc: "P S \<Longrightarrow> (countable union_of P) S"
+  by (simp add: union_of_inc)
+
+lemma countable_intersection_of_inc: "P S \<Longrightarrow> (countable intersection_of P) S"
+  by (simp add: intersection_of_inc)
+
+lemma countable_union_of_complement:
+  "(countable union_of P) S \<longleftrightarrow> (countable intersection_of (\<lambda>S. P(-S))) (-S)" 
+  (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then obtain \<U> where "countable \<U>" and \<U>: "\<U> \<subseteq> Collect P" "\<Union>\<U> = S"
+    by (metis union_of_def)
+  define \<U>' where "\<U>' \<equiv> (\<lambda>C. -C) ` \<U>"
+  have "\<U>' \<subseteq> {S. P (- S)}" "\<Inter>\<U>' = -S"
+    using \<U>'_def \<U> by auto
+  then show ?rhs
+    unfolding intersection_of_def by (metis \<U>'_def \<open>countable \<U>\<close> countable_image)
+next
+  assume ?rhs
+  then obtain \<U> where "countable \<U>" and \<U>: "\<U> \<subseteq> {S. P (- S)}" "\<Inter>\<U> = -S"
+    by (metis intersection_of_def)
+  define \<U>' where "\<U>' \<equiv> (\<lambda>C. -C) ` \<U>"
+  have "\<U>' \<subseteq> Collect P" "\<Union> \<U>' = S"
+    using \<U>'_def \<U> by auto
+  then show ?lhs
+    unfolding union_of_def
+    by (metis \<U>'_def \<open>countable \<U>\<close> countable_image)
+qed
+
+lemma countable_intersection_of_complement:
+   "(countable intersection_of P) S \<longleftrightarrow> (countable union_of (\<lambda>S. P(- S))) (- S)"
+  by (simp add: countable_union_of_complement)
+
+lemma countable_union_of_explicit:
+  assumes "P {}"
+  shows "(countable union_of P) S \<longleftrightarrow>
+         (\<exists>T. (\<forall>n::nat. P(T n)) \<and> \<Union>(range T) = S)" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then obtain \<U> where "countable \<U>" and \<U>: "\<U> \<subseteq> Collect P" "\<Union>\<U> = S"
+    by (metis union_of_def)
+  then show ?rhs
+    by (metis SUP_bot Sup_empty assms from_nat_into mem_Collect_eq range_from_nat_into subsetD)
+next
+  assume ?rhs
+  then show ?lhs
+    by (metis countableI_type countable_image image_subset_iff mem_Collect_eq union_of_def)
+qed
+
+lemma countable_union_of_ascending:
+  assumes empty: "P {}" and Un: "\<And>T U. \<lbrakk>P T; P U\<rbrakk> \<Longrightarrow> P(T \<union> U)"
+  shows "(countable union_of P) S \<longleftrightarrow>
+         (\<exists>T. (\<forall>n. P(T n)) \<and> (\<forall>n. T n \<subseteq> T(Suc n)) \<and> \<Union>(range T) = S)" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then obtain T where T: "\<And>n::nat. P(T n)" "\<Union>(range T) = S"
+    by (meson empty countable_union_of_explicit)
+  have "P (\<Union> (T ` {..n}))" for n
+    by (induction n) (auto simp: atMost_Suc Un T)
+  with T show ?rhs
+    by (rule_tac x="\<lambda>n. \<Union>k\<le>n. T k" in exI) force
+next
+  assume ?rhs
+  then show ?lhs
+    using empty countable_union_of_explicit by auto
+qed
+
+lemma countable_union_of_idem [simp]:
+  "countable union_of countable union_of P = countable union_of P"  (is "?lhs=?rhs")
+proof
+  fix S
+  show "(countable union_of countable union_of P) S = (countable union_of P) S"
+  proof
+    assume L: "?lhs S"
+    then obtain \<U> where "countable \<U>" and \<U>: "\<U> \<subseteq> Collect (countable union_of P)" "\<Union>\<U> = S"
+      by (metis union_of_def)
+    then have "\<forall>U \<in> \<U>. \<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> Collect P \<and> U = \<Union>\<V>"
+      by (metis Ball_Collect union_of_def)
+    then obtain \<F> where \<F>: "\<forall>U \<in> \<U>. countable (\<F> U) \<and> \<F> U \<subseteq> Collect P \<and> U = \<Union>(\<F> U)"
+      by metis
+    have "countable (\<Union> (\<F> ` \<U>))"
+      using \<F> \<open>countable \<U>\<close> by blast
+    moreover have "\<Union> (\<F> ` \<U>) \<subseteq> Collect P"
+      by (simp add: Sup_le_iff \<F>)
+    moreover have "\<Union> (\<Union> (\<F> ` \<U>)) = S"
+      by auto (metis Union_iff \<F> \<U>(2))+
+    ultimately show "?rhs S"
+      by (meson union_of_def)
+  qed (simp add: countable_union_of_inc)
+qed
+
+lemma countable_intersection_of_idem [simp]:
+   "countable intersection_of countable intersection_of P =
+        countable intersection_of P"
+  by (force simp: countable_intersection_of_complement)
+
+lemma countable_union_of_Union:
+   "\<lbrakk>countable \<U>; \<And>S. S \<in> \<U> \<Longrightarrow> (countable union_of P) S\<rbrakk>
+        \<Longrightarrow> (countable union_of P) (\<Union> \<U>)"
+  by (metis Ball_Collect countable_union_of_idem union_of_def)
+
+lemma countable_union_of_UN:
+   "\<lbrakk>countable I; \<And>i. i \<in> I \<Longrightarrow> (countable union_of P) (U i)\<rbrakk>
+        \<Longrightarrow> (countable union_of P) (\<Union>i\<in>I. U i)"
+  by (metis (mono_tags, lifting) countable_image countable_union_of_Union imageE)
+
+lemma countable_union_of_Un:
+  "\<lbrakk>(countable union_of P) S; (countable union_of P) T\<rbrakk>
+           \<Longrightarrow> (countable union_of P) (S \<union> T)"
+  by (smt (verit) Union_Un_distrib countable_Un le_sup_iff union_of_def)
+
+lemma countable_intersection_of_Inter:
+   "\<lbrakk>countable \<U>; \<And>S. S \<in> \<U> \<Longrightarrow> (countable intersection_of P) S\<rbrakk>
+        \<Longrightarrow> (countable intersection_of P) (\<Inter> \<U>)"
+  by (metis countable_intersection_of_idem intersection_of_def mem_Collect_eq subsetI)
+
+lemma countable_intersection_of_INT:
+   "\<lbrakk>countable I; \<And>i. i \<in> I \<Longrightarrow> (countable intersection_of P) (U i)\<rbrakk>
+        \<Longrightarrow> (countable intersection_of P) (\<Inter>i\<in>I. U i)"
+  by (metis (mono_tags, lifting) countable_image countable_intersection_of_Inter imageE)
+
+lemma countable_intersection_of_inter:
+   "\<lbrakk>(countable intersection_of P) S; (countable intersection_of P) T\<rbrakk>
+           \<Longrightarrow> (countable intersection_of P) (S \<inter> T)"
+  by (simp add: countable_intersection_of_complement countable_union_of_Un)
+
+lemma countable_union_of_Int:
+  assumes S: "(countable union_of P) S" and T: "(countable union_of P) T"
+    and Int: "\<And>S T. P S \<and> P T \<Longrightarrow> P(S \<inter> T)"
+  shows "(countable union_of P) (S \<inter> T)"
+proof -
+  obtain \<U> where "countable \<U>" and \<U>: "\<U> \<subseteq> Collect P" "\<Union>\<U> = S"
+    using S by (metis union_of_def)
+  obtain \<V> where "countable \<V>" and \<V>: "\<V> \<subseteq> Collect P" "\<Union>\<V> = T"
+    using T by (metis union_of_def)
+  have "\<And>U V. \<lbrakk>U \<in> \<U>; V \<in> \<V>\<rbrakk> \<Longrightarrow> (countable union_of P) (U \<inter> V)"
+    using \<U> \<V> by (metis Ball_Collect countable_union_of_inc local.Int)
+  then have "(countable union_of P) (\<Union>U\<in>\<U>. \<Union>V\<in>\<V>. U \<inter> V)"
+    by (meson \<open>countable \<U>\<close> \<open>countable \<V>\<close> countable_union_of_UN)
+  moreover have "S \<inter> T = (\<Union>U\<in>\<U>. \<Union>V\<in>\<V>. U \<inter> V)"
+    by (simp add: \<U> \<V>)
+  ultimately show ?thesis
+    by presburger
+qed
+
+lemma countable_intersection_of_union:
+  assumes S: "(countable intersection_of P) S" and T: "(countable intersection_of P) T"
+    and Un: "\<And>S T. P S \<and> P T \<Longrightarrow> P(S \<union> T)"
+  shows "(countable intersection_of P) (S \<union> T)"
+  by (metis (mono_tags, lifting) Compl_Int S T Un compl_sup countable_intersection_of_complement countable_union_of_Int)
+
 end
diff -r 01c88cf514fc -r 7f240b0dabd9 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Set.thy	Tue May 02 15:17:39 2023 +0100
@@ -1946,6 +1946,9 @@
 lemma disjnt_Un2 [simp]: "disjnt C (A \<union> B) \<longleftrightarrow> disjnt C A \<and> disjnt C B"
   by (auto simp: disjnt_def)
 
+lemma disjnt_Diff1: "disjnt (X-Y) (U-V)" and disjnt_Diff2: "disjnt (U-V) (X-Y)" if "X \<subseteq> V"
+  using that by (auto simp: disjnt_def)
+
 lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
   unfolding disjnt_def pairwise_def by fast
 
diff -r 01c88cf514fc -r 7f240b0dabd9 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Set_Interval.thy	Tue May 02 15:17:39 2023 +0100
@@ -280,8 +280,8 @@
 context order
 begin
 
-lemma atLeastatMost_empty[simp]:
-  "b < a \<Longrightarrow> {a..b} = {}"
+lemma atLeastatMost_empty[simp]: "b < a \<Longrightarrow> {a..b} = {}" 
+  and atLeastatMost_empty'[simp]: "\<not> a \<le> b \<Longrightarrow> {a..b} = {}"
   by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
 
 lemma atLeastLessThan_empty[simp]: