# HG changeset patch
# User paulson
# Date 1683106520 -3600
# Node ID 041678c7f1476a7a18d861b3f64e0595b8bfb280
# Parent  faaff590bd9e483564c0ec99eb292a169f9fd47d# Parent  7f240b0dabd9666cd69e44400bc97775c83bd803
merged

diff -r faaff590bd9e -r 041678c7f147 src/HOL/Analysis/Abstract_Limits.thy
--- a/src/HOL/Analysis/Abstract_Limits.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Abstract_Limits.thy	Wed May 03 10:35:20 2023 +0100
@@ -47,6 +47,9 @@
 definition limitin :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
   "limitin X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
 
+lemma limitinD: "\<lbrakk>limitin X f l F; openin X U; l \<in> U\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. f x \<in> U) F"
+  by (simp add: limitin_def)
+
 lemma limitin_canonical_iff [simp]: "limitin euclidean f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
   by (auto simp: limitin_def tendsto_def)
 
diff -r faaff590bd9e -r 041678c7f147 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Wed May 03 10:35:20 2023 +0100
@@ -174,6 +174,18 @@
   shows "closedin U (S - T)"
   by (metis Int_Diff cT closedin_Int closedin_subset inf.orderE oS openin_closedin_eq)
 
+lemma all_openin: "(\<forall>U. openin X U \<longrightarrow> P U) \<longleftrightarrow> (\<forall>U. closedin X U \<longrightarrow> P (topspace X - U))"
+  by (metis Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq)
+
+lemma all_closedin: "(\<forall>U. closedin X U \<longrightarrow> P U) \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> P (topspace X - U))"
+  by (metis Diff_Diff_Int closedin_subset inf.absorb_iff2 openin_closedin_eq)
+
+lemma ex_openin: "(\<exists>U. openin X U \<and> P U) \<longleftrightarrow> (\<exists>U. closedin X U \<and> P (topspace X - U))"
+  by (metis Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq)
+
+lemma ex_closedin: "(\<exists>U. closedin X U \<and> P U) \<longleftrightarrow> (\<exists>U. openin X U \<and> P (topspace X - U))"
+  by (metis Diff_Diff_Int closedin_subset inf.absorb_iff2 openin_closedin_eq)
+
 
 subsection\<open>The discrete topology\<close>
 
@@ -285,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)
@@ -1371,7 +1387,7 @@
   by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure)
 
 lemma closure_of_Union_subset: "\<Union>((\<lambda>S. X closure_of S) ` \<A>) \<subseteq> X closure_of (\<Union>\<A>)"
-  by clarify (meson Union_upper closure_of_mono subsetD)
+  by (simp add: SUP_le_iff Sup_upper closure_of_mono)
 
 lemma closure_of_locally_finite_Union:
   assumes "locally_finite_in X \<A>" 
@@ -1867,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
@@ -2151,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"
@@ -2245,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>
@@ -2766,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)
 
@@ -2966,7 +3313,7 @@
     by (metis closure_of_eq)
 qed
 
-lemma connectedin_inter_frontier_of:
+lemma connectedin_Int_frontier_of:
   assumes "connectedin X S" "S \<inter> T \<noteq> {}" "S - T \<noteq> {}"
   shows "S \<inter> X frontier_of T \<noteq> {}"
 proof -
@@ -3068,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
@@ -3360,7 +3707,7 @@
 corollary compact_space_imp_nest:
   fixes C :: "nat \<Rightarrow> 'a set"
   assumes "compact_space X" and clo: "\<And>n. closedin X (C n)"
-    and ne: "\<And>n. C n \<noteq> {}" and inc: "\<And>m n. m \<le> n \<Longrightarrow> C n \<subseteq> C m"
+    and ne: "\<And>n. C n \<noteq> {}" and dec: "decseq C"
   shows "(\<Inter>n. C n) \<noteq> {}"
 proof -
   let ?\<U> = "range (\<lambda>n. \<Inter>m \<le> n. C m)"
@@ -3370,8 +3717,8 @@
   proof -
     obtain n where "\<And>k. k \<in> K \<Longrightarrow> k \<le> n"
       using Max.coboundedI \<open>finite K\<close> by blast
-    with inc have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
-    by blast
+    with dec have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
+      unfolding decseq_def by blast
   with ne [of n] show ?thesis
     by blast
   qed
@@ -3556,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 faaff590bd9e -r 041678c7f147 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed May 03 10:35:20 2023 +0100
@@ -1138,6 +1138,20 @@
     by (force simp: retract_of_space_def)
 qed
 
+lemma retract_of_space_trans:
+  assumes "S retract_of_space X"  "T retract_of_space subtopology X S"
+  shows "T retract_of_space X"
+  using assms
+  apply (simp add: retract_of_space_retraction_maps)
+  by (metis id_comp inf.absorb_iff2 retraction_maps_compose subtopology_subtopology)
+
+lemma retract_of_space_subtopology:
+  assumes "S retract_of_space X"  "S \<subseteq> U"
+  shows "S retract_of_space subtopology X U"
+  using assms
+  apply (clarsimp simp: retract_of_space_def)
+  by (metis continuous_map_from_subtopology inf.absorb2 subtopology_subtopology)
+
 lemma retract_of_space_clopen:
   assumes "openin X S" "closedin X S" "S = {} \<Longrightarrow> topspace X = {}"
   shows "S retract_of_space X"
@@ -1194,6 +1208,13 @@
   using embedding_map_imp_homeomorphic_space homeomorphic_space_sym section_imp_embedding_map
         section_map_def by blast
 
+lemma hereditary_imp_retractive_property:
+  assumes "\<And>X S. P X \<Longrightarrow> P(subtopology X S)" 
+          "\<And>X X'. X homeomorphic_space X' \<Longrightarrow> (P X \<longleftrightarrow> Q X')"
+  assumes "retraction_map X X' r" "P X"
+  shows "Q X'"
+  by (meson assms retraction_map_def retraction_maps_section_image2)
+
 subsection\<open>Paths and path-connectedness\<close>
 
 definition pathin :: "'a topology \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool" where
diff -r faaff590bd9e -r 041678c7f147 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed May 03 10:35:20 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 faaff590bd9e -r 041678c7f147 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy	Wed May 03 10:35:20 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 faaff590bd9e -r 041678c7f147 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Homotopy.thy	Wed May 03 10:35:20 2023 +0100
@@ -156,7 +156,7 @@
   qed
   show ?thesis
     using assms
-    apply (clarsimp simp add: homotopic_with_def)
+    apply (clarsimp simp: homotopic_with_def)
     subgoal for h
       by (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI) (simp add: continuous_map_compose [OF *])
     done
@@ -211,7 +211,7 @@
     show "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
     proof 
       fix t show "t\<in>{0..1} \<Longrightarrow> P (\<lambda>x. k (t, x))"
-        by (cases "t \<le> 1/2") (auto simp add: k_def P)
+        by (cases "t \<le> 1/2") (auto simp: k_def P)
     qed
   qed
 qed
@@ -578,7 +578,7 @@
 
 proposition homotopic_paths_join:
     "\<lbrakk>homotopic_paths S p p'; homotopic_paths S q q'; pathfinish p = pathstart q\<rbrakk> \<Longrightarrow> homotopic_paths S (p +++ q) (p' +++ q')"
-  apply (clarsimp simp add: homotopic_paths_def homotopic_with_def)
+  apply (clarsimp simp: homotopic_paths_def homotopic_with_def)
   apply (rename_tac k1 k2)
   apply (rule_tac x="(\<lambda>y. ((k1 \<circ> Pair (fst y)) +++ (k2 \<circ> Pair (fst y))) (snd y))" in exI)
   apply (intro conjI continuous_intros continuous_on_homotopic_join_lemma; force simp: joinpaths_def pathstart_def pathfinish_def path_image_def)
@@ -639,8 +639,8 @@
     show "continuous_on {x \<in> ?A. snd x \<le> 1/2} (\<lambda>t. p (fst t * (2 * snd t)))"
          "continuous_on {x \<in> ?A. 1/2 \<le> snd x} (\<lambda>t. p (fst t * (1 - (2 * snd t - 1))))"
          "continuous_on ?A snd"
-      by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp add: mult_le_one)+
-  qed (auto simp add: algebra_simps)
+      by (intro continuous_on_compose2 [OF p] continuous_intros; auto simp: mult_le_one)+
+  qed (auto simp: algebra_simps)
   then show ?thesis
     using assms
     apply (subst homotopic_paths_sym_eq)
@@ -1004,7 +1004,7 @@
         by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2)
       show "(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)" if "t \<in> {0..1}" for t 
         using assms
-        unfolding joinpaths_def subpath_def by (auto simp add: divide_simps add.commute mult.commute mult.left_commute)
+        unfolding joinpaths_def subpath_def by (auto simp: divide_simps add.commute mult.commute mult.left_commute)
     qed (use False in auto)
   qed
   then show ?thesis
@@ -1062,26 +1062,24 @@
   then have "continuous_on ({0..1} \<times> {0..1}) (g \<circ> fst)"
     by (fastforce intro!: continuous_intros)+
   with g show ?thesis
-    by (auto simp add: homotopic_loops_def homotopic_with_def path_defs image_subset_iff)
+    by (auto simp: homotopic_loops_def homotopic_with_def path_defs image_subset_iff)
 qed
 
 lemma homotopic_loops_imp_path_component_value:
-   "\<lbrakk>homotopic_loops S p q; 0 \<le> t; t \<le> 1\<rbrakk>
-        \<Longrightarrow> path_component S (p t) (q t)"
-apply (clarsimp simp add: homotopic_loops_def homotopic_with_def path_defs)
+   "\<lbrakk>homotopic_loops S p q; 0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> path_component S (p t) (q t)"
+apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs)
 apply (rule_tac x="h \<circ> (\<lambda>u. (u, t))" in exI)
 apply (fastforce elim!: continuous_on_subset intro!: continuous_intros)
 done
 
 lemma homotopic_points_eq_path_component:
    "homotopic_loops S (linepath a a) (linepath b b) \<longleftrightarrow> path_component S a b"
-by (auto simp: path_component_imp_homotopic_points
-         dest: homotopic_loops_imp_path_component_value [where t=1])
+  using homotopic_loops_imp_path_component_value path_component_imp_homotopic_points by fastforce
 
 lemma path_connected_eq_homotopic_points:
-    "path_connected S \<longleftrightarrow>
+  "path_connected S \<longleftrightarrow>
       (\<forall>a b. a \<in> S \<and> b \<in> S \<longrightarrow> homotopic_loops S (linepath a a) (linepath b b))"
-by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
+  by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
 
 
 subsection\<open>Simply connected sets\<close>
@@ -1134,16 +1132,9 @@
   then show ?rhs
   using simply_connected_eq_contractible_loop_any by (blast intro: simply_connected_imp_path_connected)
 next
-  assume r: ?rhs
-  note pa = r [THEN conjunct2, rule_format]
-  show ?lhs
-  proof (clarsimp simp add: simply_connected_eq_contractible_loop_any)
-    fix p a
-    assume "path p" and "path_image p \<subseteq> S" "pathfinish p = pathstart p"
-      and "a \<in> S"
-    with pa [of p] show "homotopic_loops S p (linepath a a)"
-      using homotopic_loops_trans path_connected_eq_homotopic_points r by blast
-  qed
+  assume ?rhs
+  then show ?lhs
+    by (meson homotopic_loops_trans path_connected_eq_homotopic_points simply_connected_eq_contractible_loop_any)
 qed
 
 lemma simply_connected_eq_contractible_loop_all:
@@ -1158,19 +1149,8 @@
 next
   case False
   then obtain a where "a \<in> S" by blast
-  show ?thesis
-  proof
-    assume "simply_connected S"
-    then show ?rhs
-      using \<open>a \<in> S\<close> \<open>simply_connected S\<close> simply_connected_eq_contractible_loop_any
-      by blast
-  next
-    assume ?rhs
-    then show "simply_connected S"
-      unfolding simply_connected_eq_contractible_loop_any 
-      by (meson False homotopic_loops_refl homotopic_loops_sym homotopic_loops_trans 
-          path_component_imp_homotopic_points path_component_refl)
-  qed
+  then show ?thesis
+    by (meson False homotopic_loops_sym homotopic_loops_trans simply_connected_def simply_connected_eq_contractible_loop_any)
 qed
 
 lemma simply_connected_eq_contractible_path:
@@ -1212,19 +1192,17 @@
            "path_image q \<subseteq> S" "pathstart q = pathstart p"
            "pathfinish q = pathfinish p" for p q
   proof -
-    have "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))"
-      by (simp add: homotopic_paths_rid homotopic_paths_sym that)
-    also have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p))
-                                 (p +++ reversepath q +++ q)"
+    have "homotopic_paths S p (p +++ reversepath q +++ q)"
       using that
-      by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl homotopic_paths_sym_eq pathstart_linepath)
+      by (smt (verit, best) homotopic_paths_join homotopic_paths_linv homotopic_paths_rid homotopic_paths_sym 
+          homotopic_paths_trans pathstart_linepath)
     also have "homotopic_paths S (p +++ reversepath q +++ q)
                                  ((p +++ reversepath q) +++ q)"
       by (simp add: that homotopic_paths_assoc)
     also have "homotopic_paths S ((p +++ reversepath q) +++ q)
                                  (linepath (pathstart q) (pathstart q) +++ q)"
       using * [of "p +++ reversepath q"] that
-      by (simp add: homotopic_paths_join path_image_join)
+      by (simp add: homotopic_paths_assoc homotopic_paths_join path_image_join)
     also have "homotopic_paths S (linepath (pathstart q) (pathstart q) +++ q) q"
       using that homotopic_paths_lid by blast
     finally show ?thesis .
@@ -1291,12 +1269,12 @@
   have "\<forall>p. path p \<and>
             path_image p \<subseteq> S \<and> pathfinish p = pathstart p \<longrightarrow>
             homotopic_loops S p (linepath a a)"
-    using a apply (clarsimp simp add: homotopic_loops_def homotopic_with_def path_defs)
+    using a apply (clarsimp simp: homotopic_loops_def homotopic_with_def path_defs)
     apply (rule_tac x="(h \<circ> (\<lambda>y. (fst y, (p \<circ> snd) y)))" in exI)
     apply (intro conjI continuous_on_compose continuous_intros; force elim: continuous_on_subset)
     done
   with \<open>a \<in> S\<close> show ?thesis
-    by (auto simp add: simply_connected_eq_contractible_loop_all False)
+    by (auto simp: simply_connected_eq_contractible_loop_all False)
 qed
 
 corollary contractible_imp_connected:
@@ -1369,20 +1347,20 @@
 lemma homotopic_into_contractible:
   fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
   assumes f: "continuous_on S f" "f ` S \<subseteq> T"
-      and g: "continuous_on S g" "g ` S \<subseteq> T"
-      and T: "contractible T"
-    shows "homotopic_with_canon (\<lambda>h. True) S T f g"
-using homotopic_through_contractible [of S f T id T g id]
-by (simp add: assms contractible_imp_path_connected)
+    and g: "continuous_on S g" "g ` S \<subseteq> T"
+    and T: "contractible T"
+  shows "homotopic_with_canon (\<lambda>h. True) S T f g"
+  using homotopic_through_contractible [of S f T id T g id]
+  by (simp add: assms contractible_imp_path_connected)
 
 lemma homotopic_from_contractible:
   fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
   assumes f: "continuous_on S f" "f ` S \<subseteq> T"
-      and g: "continuous_on S g" "g ` S \<subseteq> T"
-      and "contractible S" "path_connected T"
-    shows "homotopic_with_canon (\<lambda>h. True) S T f g"
-using homotopic_through_contractible [of S id S f T id g]
-by (simp add: assms contractible_imp_path_connected)
+    and g: "continuous_on S g" "g ` S \<subseteq> T"
+    and "contractible S" "path_connected T"
+  shows "homotopic_with_canon (\<lambda>h. True) S T f g"
+  using homotopic_through_contractible [of S id S f T id g]
+  by (simp add: assms contractible_imp_path_connected)
 
 subsection\<open>Starlike sets\<close>
 
@@ -1402,8 +1380,7 @@
 proof -
   have "rel_interior S \<noteq> {}"
     by (simp add: assms rel_interior_eq_empty)
-  then obtain a where a: "a \<in> rel_interior S"  by blast
-  with ST have "a \<in> T"  by blast
+  with ST obtain a where a: "a \<in> rel_interior S" and "a \<in> T" by blast
   have "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
     by (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a]) (use assms in auto)
   then have "\<forall>x\<in>T. a \<in> T \<and> open_segment a x \<subseteq> T"
@@ -1439,7 +1416,7 @@
 lemma starlike_imp_contractible:
   fixes S :: "'a::real_normed_vector set"
   shows "starlike S \<Longrightarrow> contractible S"
-using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def)
+  using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def)
 
 lemma contractible_UNIV [simp]: "contractible (UNIV :: 'a::real_normed_vector set)"
   by (simp add: starlike_imp_contractible)
@@ -1447,27 +1424,27 @@
 lemma starlike_imp_simply_connected:
   fixes S :: "'a::real_normed_vector set"
   shows "starlike S \<Longrightarrow> simply_connected S"
-by (simp add: contractible_imp_simply_connected starlike_imp_contractible)
+  by (simp add: contractible_imp_simply_connected starlike_imp_contractible)
 
 lemma convex_imp_simply_connected:
   fixes S :: "'a::real_normed_vector set"
   shows "convex S \<Longrightarrow> simply_connected S"
-using convex_imp_starlike starlike_imp_simply_connected by blast
+  using convex_imp_starlike starlike_imp_simply_connected by blast
 
 lemma starlike_imp_path_connected:
   fixes S :: "'a::real_normed_vector set"
   shows "starlike S \<Longrightarrow> path_connected S"
-by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected)
+  by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected)
 
 lemma starlike_imp_connected:
   fixes S :: "'a::real_normed_vector set"
   shows "starlike S \<Longrightarrow> connected S"
-by (simp add: path_connected_imp_connected starlike_imp_path_connected)
+  by (simp add: path_connected_imp_connected starlike_imp_path_connected)
 
 lemma is_interval_simply_connected_1:
   fixes S :: "real set"
   shows "is_interval S \<longleftrightarrow> simply_connected S"
-using convex_imp_simply_connected is_interval_convex_1 is_interval_path_connected_1 simply_connected_imp_path_connected by auto
+  by (meson convex_imp_simply_connected is_interval_connected_1 is_interval_convex_1 simply_connected_imp_connected)
 
 lemma contractible_empty [simp]: "contractible {}"
   by (simp add: contractible_def homotopic_on_emptyI)
@@ -1476,15 +1453,8 @@
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" and TS: "rel_interior S \<subseteq> T" "T \<subseteq> closure S"
   shows "contractible T"
-proof (cases "S = {}")
-  case True
-  with assms show ?thesis
-    by (simp add: subsetCE)
-next
-  case False
-  show ?thesis
-    by (meson False assms starlike_convex_tweak_boundary_points starlike_imp_contractible)
-qed
+  by (metis assms closure_eq_empty contractible_empty empty_subsetI 
+      starlike_convex_tweak_boundary_points starlike_imp_contractible subset_antisym)
 
 lemma convex_imp_contractible:
   fixes S :: "'a::real_normed_vector set"
@@ -1494,13 +1464,13 @@
 lemma contractible_sing [simp]:
   fixes a :: "'a::real_normed_vector"
   shows "contractible {a}"
-by (rule convex_imp_contractible [OF convex_singleton])
+  by (rule convex_imp_contractible [OF convex_singleton])
 
 lemma is_interval_contractible_1:
   fixes S :: "real set"
   shows  "is_interval S \<longleftrightarrow> contractible S"
-using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1
-      is_interval_simply_connected_1 by auto
+  using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1
+    is_interval_simply_connected_1 by auto
 
 lemma contractible_Times:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
@@ -1556,9 +1526,7 @@
 lemma locally_open_subset:
   assumes "locally P S" "openin (top_of_set S) t"
     shows "locally P t"
-  using assms
-  unfolding locally_def
-  by (elim all_forward) (meson dual_order.trans openin_imp_subset openin_subset_trans openin_trans)
+  by (smt (verit, ccfv_SIG) assms order.trans locally_def openin_imp_subset openin_subset_trans openin_trans)
 
 lemma locally_diff_closed:
     "\<lbrakk>locally P S; closedin (top_of_set S) t\<rbrakk> \<Longrightarrow> locally P (S - t)"
@@ -1575,16 +1543,13 @@
     using zero_less_one by blast
   then show ?thesis
     unfolding locally_def
-    by (auto simp add: openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR)
+    by (auto simp: openin_euclidean_subtopology_iff subset_singleton_iff conj_disj_distribR)
 qed
 
 lemma locally_iff:
     "locally P S \<longleftrightarrow>
      (\<forall>T x. open T \<and> x \<in> S \<inter> T \<longrightarrow> (\<exists>U. open U \<and> (\<exists>V. P V \<and> x \<in> S \<inter> U \<and> S \<inter> U \<subseteq> V \<and> V \<subseteq> S \<inter> T)))"
-  apply (simp add: le_inf_iff locally_def openin_open, safe)
-   apply (metis IntE IntI le_inf_iff)
-  apply (metis IntI Int_subset_iff)
-  done
+  by (smt (verit) locally_def openin_open)
 
 lemma locally_Int:
   assumes S: "locally P S" and T: "locally P T"
@@ -1649,34 +1614,29 @@
     using hom by (auto simp: homeomorphism_def)
   have gw: "g ` W = S \<inter> f -` W"
     using \<open>W \<subseteq> T\<close> g by force
-  have \<circ>: "openin (top_of_set S) (g ` W)"
-  proof -
-    have "continuous_on S f"
-      using f(3) by blast
-    then show "openin (top_of_set S) (g ` W)"
-      by (simp add: gw Collect_conj_eq \<open>openin (top_of_set T) W\<close> continuous_on_open f(2))
-  qed
+  have "openin (top_of_set S) (g ` W)"
+    using \<open>openin (top_of_set T) W\<close> continuous_on_open f gw by auto
   then obtain U V
     where osu: "openin (top_of_set S) U" and uv: "P V" "g y \<in> U" "U \<subseteq> V" "V \<subseteq> g ` W"
-    using S [unfolded locally_def, rule_format, of "g ` W" "g y"] \<open>y \<in> W\<close> by force
+    by (metis S \<open>y \<in> W\<close> image_eqI locallyE)
   have "V \<subseteq> S" using uv by (simp add: gw)
   have fv: "f ` V = T \<inter> {x. g x \<in> V}"
     using \<open>f ` S = T\<close> f \<open>V \<subseteq> S\<close> by auto
+  have contvf: "continuous_on V f"
+    using \<open>V \<subseteq> S\<close> continuous_on_subset f(3) by blast
   have "f ` V \<subseteq> W"
     using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto
-  have contvf: "continuous_on V f"
-    using \<open>V \<subseteq> S\<close> continuous_on_subset f(3) by blast
-  have contvg: "continuous_on (f ` V) g"
-    using \<open>f ` V \<subseteq> W\<close> \<open>W \<subseteq> T\<close> continuous_on_subset [OF g(3)] by blast
+  then have contvg: "continuous_on (f ` V) g"
+    using \<open>W \<subseteq> T\<close> continuous_on_subset [OF g(3)] by blast
   have "V \<subseteq> g ` f ` V"
     by (metis \<open>V \<subseteq> S\<close> hom homeomorphism_def homeomorphism_of_subsets order_refl)
   then have homv: "homeomorphism V (f ` V) f g"
-    using \<open>V \<subseteq> S\<close> f by (auto simp add: homeomorphism_def contvf contvg)
+    using \<open>V \<subseteq> S\<close> f by (auto simp: homeomorphism_def contvf contvg)
   have "openin (top_of_set (g ` T)) U"
     using \<open>g ` T = S\<close> by (simp add: osu)
-  then have 1: "openin (top_of_set T) (T \<inter> g -` U)"
+  then have "openin (top_of_set T) (T \<inter> g -` U)"
     using \<open>continuous_on T g\<close> continuous_on_open [THEN iffD1] by blast
-  have 2: "\<exists>V. Q V \<and> y \<in> (T \<inter> g -` U) \<and> (T \<inter> g -` U) \<subseteq> V \<and> V \<subseteq> W"
+  moreover have "\<exists>V. Q V \<and> y \<in> (T \<inter> g -` U) \<and> (T \<inter> g -` U) \<subseteq> V \<and> V \<subseteq> W"
   proof (intro exI conjI)
     show "Q (f ` V)"
       using Q homv \<open>P V\<close> by blast
@@ -1687,44 +1647,28 @@
     show "f ` V \<subseteq> W"
       using \<open>f ` V \<subseteq> W\<close> by blast
   qed
-  show "\<exists>U. openin (top_of_set T) U \<and> (\<exists>v. Q v \<and> y \<in> U \<and> U \<subseteq> v \<and> v \<subseteq> W)"
-    by (meson 1 2)
+  ultimately show "\<exists>U. openin (top_of_set T) U \<and> (\<exists>v. Q v \<and> y \<in> U \<and> U \<subseteq> v \<and> v \<subseteq> W)"
+    by meson
 qed
 
 lemma homeomorphism_locally:
   fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
-  assumes hom: "homeomorphism S T f g"
-      and eq: "\<And>S T. homeomorphism S T f g \<Longrightarrow> (P S \<longleftrightarrow> Q T)"
+  assumes "homeomorphism S T f g"
+      and "\<And>S T. homeomorphism S T f g \<Longrightarrow> (P S \<longleftrightarrow> Q T)"
     shows "locally P S \<longleftrightarrow> locally Q T"
-     (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  then show ?rhs
-    using eq hom homeomorphism_locally_imp by blast
-next
-  assume ?rhs
-  then show ?lhs
-    using eq homeomorphism_sym homeomorphism_symD [OF hom] 
-    by (blast intro: homeomorphism_locally_imp) 
-qed
+  by (smt (verit) assms homeomorphism_locally_imp homeomorphism_symD)
 
 lemma homeomorphic_locally:
   fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
   assumes hom: "S homeomorphic T"
           and iff: "\<And>X Y. X homeomorphic Y \<Longrightarrow> (P X \<longleftrightarrow> Q Y)"
     shows "locally P S \<longleftrightarrow> locally Q T"
-proof -
-  obtain f g where hom: "homeomorphism S T f g"
-    using assms by (force simp: homeomorphic_def)
-  then show ?thesis
-    using homeomorphic_def local.iff
-    by (blast intro!: homeomorphism_locally)
-qed
+  by (smt (verit, ccfv_SIG) hom homeomorphic_def homeomorphism_locally homeomorphism_locally_imp iff)
 
 lemma homeomorphic_local_compactness:
   fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
   shows "S homeomorphic T \<Longrightarrow> locally compact S \<longleftrightarrow> locally compact T"
-by (simp add: homeomorphic_compactness homeomorphic_locally)
+  by (simp add: homeomorphic_compactness homeomorphic_locally)
 
 lemma locally_translation:
   fixes P :: "'a :: real_normed_vector set \<Rightarrow> bool"
@@ -1746,7 +1690,7 @@
       and oo: "\<And>T. openin (top_of_set S) T \<Longrightarrow> openin (top_of_set (f ` S)) (f ` T)"
       and Q: "\<And>T. \<lbrakk>T \<subseteq> S; P T\<rbrakk> \<Longrightarrow> Q(f ` T)"
     shows "locally Q (f ` S)"
-proof (clarsimp simp add: locally_def)
+proof (clarsimp simp: locally_def)
   fix W y
   assume oiw: "openin (top_of_set (f ` S)) W" and "y \<in> W"
   then have "W \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
@@ -1756,8 +1700,7 @@
     using \<open>W \<subseteq> f ` S\<close> \<open>y \<in> W\<close> by blast
   then obtain U V
     where "openin (top_of_set S) U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> S \<inter> f -` W"
-    using P [unfolded locally_def, rule_format, of "(S \<inter> f -` W)" x] oivf \<open>y \<in> W\<close>
-    by auto
+    by (metis IntI P \<open>y \<in> W\<close> locallyE oivf vimageI)
   then have "openin (top_of_set (f ` S)) (f ` U)"
     by (simp add: oo)
   then show "\<exists>X. openin (top_of_set (f ` S)) X \<and> (\<exists>Y. Q Y \<and> y \<in> X \<and> X \<subseteq> Y \<and> Y \<subseteq> W)"
@@ -1778,17 +1721,16 @@
 proof -
   let ?A = "{b. \<exists>T. openin (top_of_set S) T \<and> b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
   let ?B = "{b. \<exists>T. openin (top_of_set S) T \<and> b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> \<not> Q x)}"
-  have 1: "openin (top_of_set S) ?A"
-    by (subst openin_subopen, blast)
-  have 2: "openin (top_of_set S) ?B"
-    by (subst openin_subopen, blast)
-  have \<section>: "?A \<inter> ?B = {}"
+  have "?A \<inter> ?B = {}"
     by (clarsimp simp: set_eq_iff) (metis (no_types, opaque_lifting) Int_iff opD openin_Int)
-  have *: "S \<subseteq> ?A \<union> ?B"
+  moreover have "S \<subseteq> ?A \<union> ?B"
     by clarsimp (meson opI)
-  have "?A = {} \<or> ?B = {}"
-    using \<open>connected S\<close> [unfolded connected_openin, simplified, rule_format, OF 1 \<section> * 2] 
-    by blast
+  moreover have "openin (top_of_set S) ?A"
+    by (subst openin_subopen, blast)
+  moreover have "openin (top_of_set S) ?B"
+    by (subst openin_subopen, blast)
+  ultimately have "?A = {} \<or> ?B = {}"
+    by (metis (no_types, lifting) \<open>connected S\<close> connected_openin)
   then show ?thesis
     by clarsimp (meson opI etc)
 qed
@@ -1851,15 +1793,11 @@
   shows "locally (\<lambda>U. f constant_on U) S \<longleftrightarrow> f constant_on S" (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then have "\<And>a. a \<in> S \<Longrightarrow> \<exists>T. openin (top_of_set S) T \<and> a \<in> T \<and> (\<forall>x\<in>T. f x = f a)"
-    unfolding locally_def
-    by (metis (mono_tags, opaque_lifting) constant_on_def constant_on_subset openin_subtopology_self)
   then show ?rhs
-    using assms
-    by (simp add: locally_constant_imp_constant)
+    by (smt (verit, del_insts) assms constant_on_def locally_constant_imp_constant locally_def openin_subtopology_self subset_iff)
 next
   assume ?rhs then show ?lhs
-    using assms by (metis constant_on_subset locallyI openin_imp_subset order_refl)
+    by (metis constant_on_subset locallyI openin_imp_subset order_refl)
 qed
 
 
@@ -1938,10 +1876,8 @@
   proof
     fix x
     assume "x \<in> S"
-    then obtain e where "e>0" and e: "closed (cball x e \<inter> S)"
-      using R by blast
-    then have "compact (cball x e \<inter> S)"
-      by (simp add: bounded_Int compact_eq_bounded_closed)
+    then obtain e where "e>0" and "compact (cball x e \<inter> S)"
+      by (metis Int_commute compact_Int_closed compact_cball inf.right_idem R)
     moreover have "\<forall>y\<in>ball x e \<inter> S. \<exists>\<epsilon>>0. cball y \<epsilon> \<inter> S \<subseteq> ball x e"
       by (meson Elementary_Metric_Spaces.open_ball IntD1 le_infI1 open_contains_cball_eq)
     moreover have "openin (top_of_set S) (ball x e \<inter> S)"
@@ -1984,10 +1920,8 @@
     have "openin (top_of_set S) (\<Union> (u ` T))"
       using T that uv by fastforce
     moreover
-    have "compact (\<Union> (v ` T))"
-      by (meson T compact_UN subset_eq that(1) uv)
-    moreover have "\<Union> (v ` T) \<subseteq> S"
-      by (metis SUP_least T(1) subset_eq that(1) uv)
+    obtain "compact (\<Union> (v ` T))" "\<Union> (v ` T) \<subseteq> S"
+      by (metis T UN_subset_iff \<open>K \<subseteq> S\<close> compact_UN subset_iff uv)
     ultimately show ?thesis
       using T by auto 
   qed
@@ -1996,7 +1930,7 @@
 next
   assume ?rhs
   then show ?lhs
-    apply (clarsimp simp add: locally_compact)
+    apply (clarsimp simp: locally_compact)
     apply (drule_tac x="{x}" in spec, simp)
     done
 qed
@@ -2014,14 +1948,7 @@
     have ope: "openin (top_of_set S) (ball x e)"
       by (meson e open_ball ball_subset_cball dual_order.trans open_subset)
     show ?thesis
-    proof (intro exI conjI)
-      let ?U = "ball x e"
-      let ?V = "cball x e"
-      show "x \<in> ?U" "?U \<subseteq> ?V" "?V \<subseteq> S" "compact ?V"
-        using \<open>e > 0\<close> e by auto
-      show "openin (top_of_set S) ?U"
-        using ope by blast
-    qed
+      by (meson \<open>0 < e\<close> ball_subset_cball centre_in_ball compact_cball e ope)
   qed
   show ?thesis
     unfolding locally_compact by (blast intro: *)
@@ -2045,13 +1972,13 @@
 
 lemma locally_compact_Int:
   fixes S :: "'a :: t2_space set"
-  shows "\<lbrakk>locally compact S; locally compact t\<rbrakk> \<Longrightarrow> locally compact (S \<inter> t)"
-by (simp add: compact_Int locally_Int)
+  shows "\<lbrakk>locally compact S; locally compact T\<rbrakk> \<Longrightarrow> locally compact (S \<inter> T)"
+  by (simp add: compact_Int locally_Int)
 
 lemma locally_compact_closedin:
   fixes S :: "'a :: heine_borel set"
-  shows "\<lbrakk>closedin (top_of_set S) t; locally compact S\<rbrakk>
-        \<Longrightarrow> locally compact t"
+  shows "\<lbrakk>closedin (top_of_set S) T; locally compact S\<rbrakk>
+        \<Longrightarrow> locally compact T"
   unfolding closedin_closed
   using closed_imp_locally_compact locally_compact_Int by blast
 
@@ -2130,12 +2057,7 @@
     obtain e2 where "e2 > 0" and e2: "closed (cball x e2 \<inter> T)"
       using LCT \<open>x \<in> T\<close> unfolding locally_compact_Int_cball by blast
     moreover have "closed (cball x (min e1 e2) \<inter> (S \<union> T))"
-    proof -
-      have "closed (cball x e1 \<inter> (cball x e2 \<inter> S))"
-        by (metis closed_Int closed_cball e1 inf_left_commute)
-      then show ?thesis
-        by (simp add: Int_Un_distrib cball_min_Int closed_Int closed_Un e2 inf_assoc)
-    qed
+      by (smt (verit) Int_Un_distrib2 Int_commute cball_min_Int closed_Int closed_Un closed_cball e1 e2 inf_left_commute)
     ultimately show ?thesis
       by (rule_tac x="min e1 e2" in exI) linarith
   qed
@@ -2298,7 +2220,7 @@
             by (simp_all add: closedin_closed_Int)
           moreover have "D \<inter> closure V1 = D \<inter> V1" "D \<inter> closure V2 = D \<inter> V2"
             using \<open>D \<subseteq> V1 \<union> V2\<close> \<open>open V1\<close> \<open>open V2\<close> V12
-            by (auto simp add: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
+            by (auto simp: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
           ultimately have cloDV1: "closedin (top_of_set D) (D \<inter> V1)"
                       and cloDV2:  "closedin (top_of_set D) (D \<inter> V2)"
             by metis+
@@ -2721,7 +2643,7 @@
   fixes S :: "'a:: real_normed_vector set"
   assumes "convex S"
   shows "locally path_connected S"
-proof (clarsimp simp add: locally_path_connected)
+proof (clarsimp simp: locally_path_connected)
   fix V x
   assume "openin (top_of_set S) V" and "x \<in> V"
   then obtain T e where  "V = S \<inter> T" "x \<in> S" "0 < e" "ball x e \<subseteq> T"
@@ -3824,7 +3746,7 @@
       show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set S)) (top_of_set S)
                            (\<lambda>(t,x). (1 - t) * x + t * z)"
         using  \<open>z \<in> S\<close> 
-        by (auto simp add: case_prod_unfold intro!: continuous_intros \<section>)
+        by (auto simp: case_prod_unfold intro!: continuous_intros \<section>)
     qed auto
   qed (simp add: contractible_space_empty)
 qed
@@ -3946,7 +3868,7 @@
     by (rule homotopic_with_compose_continuous_right [where X=S]) (use k in auto)
   moreover have "homotopic_with_canon (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
     by (rule homotopic_with_compose_continuous_left [where Y=T])
-       (use f in \<open>auto simp add: hom homotopic_with_symD\<close>)
+       (use f in \<open>auto simp: hom homotopic_with_symD\<close>)
   ultimately show ?thesis
     using that homotopic_with_trans by (fastforce simp add: o_def)
 qed
@@ -3987,7 +3909,7 @@
     by (rule homotopic_with_compose_continuous_left [where Y=S]) (use h in auto)
   moreover have "homotopic_with_canon (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
     by (rule homotopic_with_compose_continuous_right [where X=T])
-       (use f in \<open>auto simp add: hom homotopic_with_symD\<close>)
+       (use f in \<open>auto simp: hom homotopic_with_symD\<close>)
   ultimately show ?thesis
     using homotopic_with_trans by (fastforce simp add: o_def)
 qed
@@ -4123,7 +4045,7 @@
   fixes U :: "'a::euclidean_space set"
   assumes "convex U" "\<not> collinear U" "countable S"
     shows "path_connected(U - S)"
-proof (clarsimp simp add: path_connected_def)
+proof (clarsimp simp: path_connected_def)
   fix a b
   assume "a \<in> U" "a \<notin> S" "b \<in> U" "b \<notin> S"
   let ?m = "midpoint a b"
@@ -4245,7 +4167,7 @@
   next
     assume ge2: "aff_dim S \<ge> 2"
     then have "\<not> collinear S"
-    proof (clarsimp simp add: collinear_affine_hull)
+    proof (clarsimp simp: collinear_affine_hull)
       fix u v
       assume "S \<subseteq> affine hull {u, v}"
       then have "aff_dim S \<le> aff_dim {u, v}"
@@ -4282,7 +4204,7 @@
   assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S"
       and "\<not> collinear S" "countable T"
     shows "path_connected(S - T)"
-proof (clarsimp simp add: path_connected_component)
+proof (clarsimp simp: path_connected_component)
   fix x y
   assume xy: "x \<in> S" "x \<notin> T" "y \<in> S" "y \<notin> T"
   show "path_component (S - T) x y"
@@ -4483,7 +4405,7 @@
       by blast
   next
     show "cball a r \<inter> T \<subseteq> f ` (cball a r \<inter> T)"
-    proof (clarsimp simp add: dist_norm norm_minus_commute)
+    proof (clarsimp simp: dist_norm norm_minus_commute)
       fix x
       assume x: "norm (x - a) \<le> r" and "x \<in> T"
       have "\<exists>v \<in> {0..1}. ((1 - v) * r - norm ((x - a) - v *\<^sub>R (u - a))) \<bullet> 1 = 0"
@@ -4575,7 +4497,7 @@
       then show "continuous_on S gg"
         by (rule continuous_on_subset) (use ST in auto)
       show "ff ` S \<subseteq> S"
-      proof (clarsimp simp add: ff_def)
+      proof (clarsimp simp: ff_def)
         fix x
         assume "x \<in> S" and x: "dist a x < r" and "x \<in> T"
         then have "f x \<in> cball a r \<inter> T"
@@ -4584,7 +4506,7 @@
           using ST(1) \<open>x \<in> T\<close> gid hom homeomorphism_def x by fastforce
       qed
       show "gg ` S \<subseteq> S"
-      proof (clarsimp simp add: gg_def)
+      proof (clarsimp simp: gg_def)
         fix x
         assume "x \<in> S" and x: "dist a x < r" and "x \<in> T"
         then have "g x \<in> cball a r \<inter> T"
diff -r faaff590bd9e -r 041678c7f147 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed May 03 10:35:20 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 faaff590bd9e -r 041678c7f147 src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/Product_Topology.thy	Wed May 03 10:35:20 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 faaff590bd9e -r 041678c7f147 src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Analysis/T1_Spaces.thy	Wed May 03 10:35:20 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 faaff590bd9e -r 041678c7f147 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Archimedean_Field.thy	Wed May 03 10:35:20 2023 +0100
@@ -16,15 +16,10 @@
 proof -
   have "Sup (uminus ` S) = - (Inf S)"
   proof (rule antisym)
-    show "- (Inf S) \<le> Sup (uminus ` S)"
-      apply (subst minus_le_iff)
-      apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
-      apply (subst minus_le_iff)
-      apply (rule cSup_upper)
-       apply force
-      using bdd
-      apply (force simp: abs_le_iff bdd_above_def)
-      done
+    have "\<And>x. x \<in> S \<Longrightarrow> bdd_above (uminus ` S)"
+      using bdd by (force simp: abs_le_iff bdd_above_def)
+  then show "- (Inf S) \<le> Sup (uminus ` S)"
+    by (meson cInf_greatest [OF \<open>S \<noteq> {}\<close>] cSUP_upper minus_le_iff)
   next
     have *: "\<And>x. x \<in> S \<Longrightarrow> Inf S \<le> x"
       by (meson abs_le_iff bdd bdd_below_def cInf_lower minus_le_iff)
diff -r faaff590bd9e -r 041678c7f147 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed May 03 10:35:20 2023 +0100
@@ -481,6 +481,12 @@
   assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
 qed (intro cSup_eq_non_empty assms)
 
+lemma cSup_unique:
+  fixes b :: "'a :: {conditionally_complete_lattice, no_bot}"
+  assumes "\<And>c. (\<forall>x \<in> s. x \<le> c) \<longleftrightarrow> b \<le> c"
+  shows "Sup s = b"
+  by (metis assms cSup_eq order.refl)
+
 lemma cInf_eq:
   fixes a :: "'a :: {conditionally_complete_lattice, no_top}"
   assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
@@ -490,6 +496,12 @@
   assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
 qed (intro cInf_eq_non_empty assms)
 
+lemma cInf_unique:
+  fixes b :: "'a :: {conditionally_complete_lattice, no_top}"
+  assumes "\<And>c. (\<forall>x \<in> s. x \<ge> c) \<longleftrightarrow> b \<ge> c"
+  shows "Inf s = b"
+  by (meson assms cInf_eq order.refl)
+
 class conditionally_complete_linorder = conditionally_complete_lattice + linorder
 begin
 
diff -r faaff590bd9e -r 041678c7f147 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Fun.thy	Wed May 03 10:35:20 2023 +0100
@@ -1031,6 +1031,12 @@
 abbreviation strict_mono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
   where "strict_mono_on A \<equiv> monotone_on A (<) (<)"
 
+abbreviation antimono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
+  where "antimono_on A \<equiv> monotone_on A (\<le>) (\<ge>)"
+
+abbreviation strict_antimono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
+  where "strict_antimono_on A \<equiv> monotone_on A (<) (>)"
+
 lemma mono_on_def[no_atp]: "mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s)"
   by (auto simp add: monotone_on_def)
 
@@ -1265,6 +1271,32 @@
   "strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) \<Longrightarrow> mono_on A f"
   by (rule mono_onI, rule strict_mono_on_leD)
 
+lemma mono_imp_strict_mono:
+  fixes f :: "'a::order \<Rightarrow> 'b::order"
+  shows "\<lbrakk>mono_on S f; inj_on f S\<rbrakk> \<Longrightarrow> strict_mono_on S f"
+  by (auto simp add: monotone_on_def order_less_le inj_on_eq_iff)
+
+lemma strict_mono_iff_mono:
+  fixes f :: "'a::linorder \<Rightarrow> 'b::order"
+  shows "strict_mono_on S f \<longleftrightarrow> mono_on S f \<and> inj_on f S"
+proof
+  show "strict_mono_on S f \<Longrightarrow> mono_on S f \<and> inj_on f S"
+    by (simp add: strict_mono_on_imp_inj_on strict_mono_on_imp_mono_on)
+qed (auto intro: mono_imp_strict_mono)
+
+lemma antimono_imp_strict_antimono:
+  fixes f :: "'a::order \<Rightarrow> 'b::order"
+  shows "\<lbrakk>antimono_on S f; inj_on f S\<rbrakk> \<Longrightarrow> strict_antimono_on S f"
+  by (auto simp add: monotone_on_def order_less_le inj_on_eq_iff)
+
+lemma strict_antimono_iff_antimono:
+  fixes f :: "'a::linorder \<Rightarrow> 'b::order"
+  shows "strict_antimono_on S f \<longleftrightarrow> antimono_on S f \<and> inj_on f S"
+proof
+  show "strict_antimono_on S f \<Longrightarrow> antimono_on S f \<and> inj_on f S"
+    by (force simp add: monotone_on_def intro: linorder_inj_onI)
+qed (auto intro: antimono_imp_strict_antimono)
+
 lemma mono_compose: "mono Q \<Longrightarrow> mono (\<lambda>i x. Q i (f x))"
   unfolding mono_def le_fun_def by auto
 
diff -r faaff590bd9e -r 041678c7f147 src/HOL/Library/Set_Idioms.thy
--- a/src/HOL/Library/Set_Idioms.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Library/Set_Idioms.thy	Wed May 03 10:35:20 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 faaff590bd9e -r 041678c7f147 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Real.thy	Wed May 03 10:35:20 2023 +0100
@@ -1096,6 +1096,27 @@
   by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc)
 
 
+lemma inverse_Suc: "inverse (Suc n) > 0"
+  using of_nat_0_less_iff positive_imp_inverse_positive zero_less_Suc by blast
+
+lemma Archimedean_eventually_inverse:
+  fixes \<epsilon>::real shows "(\<forall>\<^sub>F n in sequentially. inverse (real (Suc n)) < \<epsilon>) \<longleftrightarrow> 0 < \<epsilon>"
+  (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    unfolding eventually_at_top_dense using inverse_Suc order_less_trans by blast
+next
+  assume ?rhs
+  then obtain N where "inverse (Suc N) < \<epsilon>"
+    using reals_Archimedean by blast
+  moreover have "inverse (Suc n) \<le> inverse (Suc N)" if "n \<ge> N" for n
+    using inverse_Suc that by fastforce
+  ultimately show ?lhs
+    unfolding eventually_sequentially
+    using order_le_less_trans by blast
+qed
+
 subsection \<open>Rationals\<close>
 
 lemma Rats_abs_iff[simp]:
diff -r faaff590bd9e -r 041678c7f147 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Set.thy	Wed May 03 10:35:20 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 faaff590bd9e -r 041678c7f147 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue May 02 08:39:48 2023 +0000
+++ b/src/HOL/Set_Interval.thy	Wed May 03 10:35:20 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]: