# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1683467573 -3600
# Node ID ffdad62bc2354c0df68169b5fb502a766068c4ba
# Parent  30f69046f120ee5c689e3c75a80254df133e59f5
Importation of additional lemmas from metric.ml

diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Analysis/Abstract_Limits.thy
--- a/src/HOL/Analysis/Abstract_Limits.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Limits.thy	Sun May 07 14:52:53 2023 +0100
@@ -41,6 +41,29 @@
   finally show ?thesis by (simp add: True)
 qed auto
 
+lemma nontrivial_limit_atin:
+   "atin X a \<noteq> bot \<longleftrightarrow> a \<in> X derived_set_of topspace X"
+proof 
+  assume L: "atin X a \<noteq> bot"
+  then have "a \<in> topspace X"
+    by (meson atin_degenerate)
+  moreover have "\<not> openin X {a}"
+    using L by (auto simp: eventually_atin trivial_limit_eq)
+  ultimately
+  show "a \<in> X derived_set_of topspace X"
+    by (auto simp: derived_set_of_topspace)
+next
+  assume a: "a \<in> X derived_set_of topspace X"
+  show "atin X a \<noteq> bot"
+  proof
+    assume "atin X a = bot"
+    then have "eventually (\<lambda>_. False) (atin X a)"
+      by simp
+    then show False
+      by (smt (verit, best) a eventually_atin in_derived_set_of insertE insert_Diff)
+  qed
+qed
+
 
 subsection\<open>Limits in a topological space\<close>
 
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Sun May 07 14:52:53 2023 +0100
@@ -3,8 +3,7 @@
 section \<open>Various Forms of Topological Spaces\<close>
 
 theory Abstract_Topological_Spaces
-  imports
-    Lindelof_Spaces Locally Sum_Topology
+  imports Lindelof_Spaces Locally Sum_Topology FSigma
 begin
 
 
@@ -1396,6 +1395,9 @@
 definition kc_space 
   where "kc_space X \<equiv> \<forall>S. compactin X S \<longrightarrow> closedin X S"
 
+lemma kc_space_euclidean: "kc_space (euclidean :: 'a::metric_space topology)"
+  by (simp add: compact_imp_closed kc_space_def)
+  
 lemma kc_space_expansive:
    "\<lbrakk>kc_space X; topspace Y = topspace X; \<And>U. openin X U \<Longrightarrow> openin Y U\<rbrakk>
       \<Longrightarrow> kc_space Y"
@@ -2911,5 +2913,619 @@
   qed (use x \<open>f x \<in> U\<close> \<open>U \<subseteq> K\<close> in auto)
 qed
 
+
+subsection\<open>Special characterizations of classes of functions into and out of R\<close>
+
+lemma monotone_map_into_euclideanreal_alt:
+  assumes "continuous_map X euclideanreal f" 
+  shows "(\<forall>k. is_interval k \<longrightarrow> connectedin X {x \<in> topspace X. f x \<in> k}) \<longleftrightarrow>
+         connected_space X \<and> monotone_map X euclideanreal f"  (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  show ?rhs
+  proof
+    show "connected_space X"
+      using L connected_space_subconnected by blast
+    have "connectedin X {x \<in> topspace X. f x \<in> {y}}" for y
+      by (metis L is_interval_1 nle_le singletonD)
+    then show "monotone_map X euclideanreal f"
+      by (simp add: monotone_map)
+  qed
+next
+  assume R: ?rhs 
+  then
+  have *: False 
+      if "a < b" "closedin X U" "closedin X V" "U \<noteq> {}" "V \<noteq> {}" "disjnt U V"
+         and UV: "{x \<in> topspace X. f x \<in> {a..b}} = U \<union> V" 
+         and dis: "disjnt U {x \<in> topspace X. f x = b}" "disjnt V {x \<in> topspace X. f x = a}" 
+       for a b U V
+  proof -
+    define E1 where "E1 \<equiv> U \<union> {x \<in> topspace X. f x \<in> {c. c \<le> a}}"
+    define E2 where "E2 \<equiv> V \<union> {x \<in> topspace X. f x \<in> {c. b \<le> c}}"
+    have "closedin X {x \<in> topspace X. f x \<le> a}" "closedin X {x \<in> topspace X. b \<le> f x}"
+      using assms continuous_map_upper_lower_semicontinuous_le by blast+
+    then have "closedin X E1" "closedin X E2"
+      unfolding E1_def E2_def using that by auto
+    moreover
+    have "E1 \<inter> E2 = {}"
+      unfolding E1_def E2_def using \<open>a<b\<close> \<open>disjnt U V\<close> dis UV
+      by (simp add: disjnt_def set_eq_iff) (smt (verit))
+    have "topspace X \<subseteq> E1 \<union> E2"
+      unfolding E1_def E2_def using UV by fastforce
+    have "E1 = {} \<or> E2 = {}"
+      using R connected_space_closedin
+      using \<open>E1 \<inter> E2 = {}\<close> \<open>closedin X E1\<close> \<open>closedin X E2\<close> \<open>topspace X \<subseteq> E1 \<union> E2\<close> by blast
+    then show False
+      using E1_def E2_def \<open>U \<noteq> {}\<close> \<open>V \<noteq> {}\<close> by fastforce
+  qed
+  show ?lhs
+  proof (intro strip)
+    fix K :: "real set"
+    assume "is_interval K"
+    have False
+      if "a \<in> K" "b \<in> K" and clo: "closedin X U" "closedin X V" 
+         and UV: "{x. x \<in> topspace X \<and> f x \<in> K} \<subseteq> U \<union> V"
+                 "U \<inter> V \<inter> {x. x \<in> topspace X \<and> f x \<in> K} = {}" 
+         and nondis: "\<not> disjnt U {x. x \<in> topspace X \<and> f x = a}"
+                     "\<not> disjnt V {x. x \<in> topspace X \<and> f x = b}" 
+     for a b U V
+    proof -
+      have "\<forall>y. connectedin X {x. x \<in> topspace X \<and> f x = y}"
+        using R monotone_map by fastforce
+      then have **: False if "p \<in> U \<and> q \<in> V \<and> f p = f q \<and> f q \<in> K" for p q
+        unfolding connectedin_closedin
+        using \<open>a \<in> K\<close> \<open>b \<in> K\<close> UV clo that 
+        by (smt (verit, ccfv_threshold) closedin_subset disjoint_iff mem_Collect_eq subset_iff)
+      consider "a < b" | "a = b" | "b < a"
+        by linarith
+      then show ?thesis
+      proof cases
+        case 1
+        define W where "W \<equiv> {x \<in> topspace X. f x \<in> {a..b}}"
+        have "closedin X W"
+          unfolding W_def
+          by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin continuous_map_closedin)
+        show ?thesis
+        proof (rule * [OF 1 , of "U \<inter> W" "V \<inter> W"])
+          show "closedin X (U \<inter> W)" "closedin X (V \<inter> W)"
+            using \<open>closedin X W\<close> clo by auto
+          show "U \<inter> W \<noteq> {}" "V \<inter> W \<noteq> {}"
+            using nondis 1 by (auto simp: disjnt_iff W_def)
+          show "disjnt (U \<inter> W) (V \<inter> W)"
+            using \<open>is_interval K\<close> unfolding is_interval_1 disjnt_iff W_def
+            by (metis (mono_tags, lifting) \<open>a \<in> K\<close> \<open>b \<in> K\<close> ** Int_Collect atLeastAtMost_iff)
+          have "\<And>x. \<lbrakk>x \<in> topspace X; a \<le> f x; f x \<le> b\<rbrakk> \<Longrightarrow> x \<in> U \<or> x \<in> V"
+            using \<open>a \<in> K\<close> \<open>b \<in> K\<close> \<open>is_interval K\<close> UV unfolding is_interval_1 disjnt_iff
+            by blast
+          then show "{x \<in> topspace X. f x \<in> {a..b}} = U \<inter> W \<union> V \<inter> W"
+            by (auto simp: W_def)
+          show "disjnt (U \<inter> W) {x \<in> topspace X. f x = b}" "disjnt (V \<inter> W) {x \<in> topspace X. f x = a}"
+            using ** \<open>a \<in> K\<close> \<open>b \<in> K\<close> nondis by (force simp: disjnt_iff)+
+        qed
+      next
+        case 2
+        then show ?thesis
+          using ** nondis \<open>b \<in> K\<close> by (force simp add: disjnt_iff)
+      next
+        case 3
+        define W where "W \<equiv> {x \<in> topspace X. f x \<in> {b..a}}"
+        have "closedin X W"
+          unfolding W_def
+          by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin continuous_map_closedin)
+        show ?thesis
+        proof (rule * [OF 3, of "V \<inter> W" "U \<inter> W"])
+          show "closedin X (U \<inter> W)" "closedin X (V \<inter> W)"
+            using \<open>closedin X W\<close> clo by auto
+          show "U \<inter> W \<noteq> {}" "V \<inter> W \<noteq> {}"
+            using nondis 3 by (auto simp: disjnt_iff W_def)
+          show "disjnt (V \<inter> W) (U \<inter> W)"
+            using \<open>is_interval K\<close> unfolding is_interval_1 disjnt_iff W_def
+            by (metis (mono_tags, lifting) \<open>a \<in> K\<close> \<open>b \<in> K\<close> ** Int_Collect atLeastAtMost_iff)
+          have "\<And>x. \<lbrakk>x \<in> topspace X; b \<le> f x; f x \<le> a\<rbrakk> \<Longrightarrow> x \<in> U \<or> x \<in> V"
+            using \<open>a \<in> K\<close> \<open>b \<in> K\<close> \<open>is_interval K\<close> UV unfolding is_interval_1 disjnt_iff
+            by blast
+          then show "{x \<in> topspace X. f x \<in> {b..a}} = V \<inter> W \<union> U \<inter> W"
+            by (auto simp: W_def)
+          show "disjnt (V \<inter> W) {x \<in> topspace X. f x = a}" "disjnt (U \<inter> W) {x \<in> topspace X. f x = b}"
+            using ** \<open>a \<in> K\<close> \<open>b \<in> K\<close> nondis by (force simp: disjnt_iff)+
+        qed      
+      qed
+    qed
+    then show "connectedin X {x \<in> topspace X. f x \<in> K}"
+      unfolding connectedin_closedin disjnt_iff by blast
+  qed
+qed
+
+lemma monotone_map_into_euclideanreal:
+   "\<lbrakk>connected_space X; continuous_map X euclideanreal f\<rbrakk>
+    \<Longrightarrow> monotone_map X euclideanreal f \<longleftrightarrow>
+        (\<forall>k. is_interval k \<longrightarrow> connectedin X {x \<in> topspace X. f x \<in> k})"
+  by (simp add: monotone_map_into_euclideanreal_alt)
+
+lemma monotone_map_euclideanreal_alt:
+   "(\<forall>I::real set. is_interval I \<longrightarrow> is_interval {x::real. x \<in> S \<and> f x \<in> I}) \<longleftrightarrow>
+    is_interval S \<and> (mono_on S f \<or> antimono_on S f)" (is "?lhs=?rhs")
+proof
+  assume L [rule_format]: ?lhs 
+  show ?rhs
+  proof
+    show "is_interval S"
+      using L is_interval_1 by auto
+    have False if "a \<in> S" "b \<in> S" "c \<in> S" "a<b" "b<c" and d: "f a < f b \<and> f c < f b \<or> f a > f b \<and> f c > f b" for a b c
+      using d
+    proof
+      assume "f a < f b \<and> f c < f b"
+      then show False
+        using L [of "{y.  y < f b}"] unfolding is_interval_1
+        by (smt (verit, best) mem_Collect_eq that)
+    next
+      assume "f b < f a \<and> f b < f c"
+      then show False
+        using L [of "{y.  y > f b}"] unfolding is_interval_1
+        by (smt (verit, best) mem_Collect_eq that)
+    qed
+    then show "mono_on S f \<or> monotone_on S (\<le>) (\<ge>) f"
+      unfolding monotone_on_def by (smt (verit))
+  qed
+next
+  assume ?rhs then show ?lhs
+    unfolding is_interval_1 monotone_on_def by simp meson
+qed
+
+
+lemma monotone_map_euclideanreal:
+  fixes S :: "real set"
+  shows
+   "\<lbrakk>is_interval S; continuous_on S f\<rbrakk> \<Longrightarrow> 
+    monotone_map (top_of_set S) euclideanreal f \<longleftrightarrow> (mono_on S f \<or> monotone_on S (\<le>) (\<ge>) f)"
+  using monotone_map_euclideanreal_alt 
+  by (simp add: monotone_map_into_euclideanreal connectedin_subtopology is_interval_connected_1)
+
+lemma injective_eq_monotone_map:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "is_interval S" "continuous_on S f"
+  shows "inj_on f S \<longleftrightarrow> strict_mono_on S f \<or> strict_antimono_on S f"
+  by (metis assms injective_imp_monotone_map monotone_map_euclideanreal strict_antimono_iff_antimono 
+        strict_mono_iff_mono top_greatest topspace_euclidean topspace_euclidean_subtopology)
+
+
+subsection\<open>Normal spaces including Urysohn's lemma and the Tietze extension theorem\<close>
+
+definition normal_space 
+  where "normal_space X \<equiv>
+        \<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T 
+              \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V)"
+
+lemma normal_space_retraction_map_image:
+  assumes r: "retraction_map X Y r" and X: "normal_space X"
+  shows "normal_space Y"
+  unfolding normal_space_def
+proof clarify
+  fix S T
+  assume "closedin Y S" and "closedin Y T" and "disjnt S T"
+  obtain r' where r': "retraction_maps X Y r r'"
+    using r retraction_map_def by blast
+  have "closedin X {x \<in> topspace X. r x \<in> S}" "closedin X {x \<in> topspace X. r x \<in> T}"
+    using closedin_continuous_map_preimage \<open>closedin Y S\<close> \<open>closedin Y T\<close> r'
+    by (auto simp: retraction_maps_def)
+  moreover
+  have "disjnt {x \<in> topspace X. r x \<in> S} {x \<in> topspace X. r x \<in> T}"
+    using \<open>disjnt S T\<close> by (auto simp: disjnt_def)
+  ultimately
+  obtain U V where UV: "openin X U \<and> openin X V \<and> {x \<in> topspace X. r x \<in> S} \<subseteq> U \<and> {x \<in> topspace X. r x \<in> T} \<subseteq> V" "disjnt U V"
+    by (meson X normal_space_def)
+  show "\<exists>U V. openin Y U \<and> openin Y V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
+  proof (intro exI conjI)
+    show "openin Y {x \<in> topspace Y. r' x \<in> U}" "openin Y {x \<in> topspace Y. r' x \<in> V}"
+      using openin_continuous_map_preimage UV r'
+      by (auto simp: retraction_maps_def)
+    show "S \<subseteq> {x \<in> topspace Y. r' x \<in> U}" "T \<subseteq> {x \<in> topspace Y. r' x \<in> V}"
+      using openin_continuous_map_preimage UV r' \<open>closedin Y S\<close> \<open>closedin Y T\<close> 
+      by (auto simp add: closedin_def continuous_map_closedin retraction_maps_def subset_iff)
+    show "disjnt {x \<in> topspace Y. r' x \<in> U} {x \<in> topspace Y. r' x \<in> V}"
+      using \<open>disjnt U V\<close> by (auto simp: disjnt_def)
+  qed
+qed
+
+lemma homeomorphic_normal_space:
+   "X homeomorphic_space Y \<Longrightarrow> normal_space X \<longleftrightarrow> normal_space Y"
+  unfolding homeomorphic_space_def
+  by (meson homeomorphic_imp_retraction_maps homeomorphic_maps_sym normal_space_retraction_map_image retraction_map_def)
+
+lemma normal_space:
+  "normal_space X \<longleftrightarrow>
+    (\<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T
+          \<longrightarrow> (\<exists>U. openin X U \<and> S \<subseteq> U \<and> disjnt T (X closure_of U)))"
+proof -
+  have "(\<exists>V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V) \<longleftrightarrow> openin X U \<and> S \<subseteq> U \<and> disjnt T (X closure_of U)"
+    (is "?lhs=?rhs")
+    if "closedin X S" "closedin X T" "disjnt S T" for S T U
+  proof
+    show "?lhs \<Longrightarrow> ?rhs"
+      by (smt (verit, best) disjnt_iff in_closure_of subsetD)
+    assume R: ?rhs
+    then have "(U \<union> S) \<inter> (topspace X - X closure_of U) = {}"
+      by (metis Diff_eq_empty_iff Int_Diff Int_Un_eq(4) closure_of_subset inf.orderE openin_subset)
+    moreover have "T \<subseteq> topspace X - X closure_of U"
+      by (meson DiffI R closedin_subset disjnt_iff subsetD subsetI that(2))
+    ultimately show ?lhs
+      by (metis R closedin_closure_of closedin_def disjnt_def sup.orderE)
+  qed
+  then show ?thesis
+    unfolding normal_space_def by meson
+qed
+
+lemma normal_space_alt:
+   "normal_space X \<longleftrightarrow>
+    (\<forall>S U. closedin X S \<and> openin X U \<and> S \<subseteq> U \<longrightarrow> (\<exists>V. openin X V \<and> S \<subseteq> V \<and> X closure_of V \<subseteq> U))"
+proof -
+  have "\<exists>V. openin X V \<and> S \<subseteq> V \<and> X closure_of V \<subseteq> U"
+    if "\<And>T. closedin X T \<longrightarrow> disjnt S T \<longrightarrow> (\<exists>U. openin X U \<and> S \<subseteq> U \<and> disjnt T (X closure_of U))"
+       "closedin X S" "openin X U" "S \<subseteq> U"
+    for S U
+    using that 
+    by (smt (verit) Diff_eq_empty_iff Int_Diff closure_of_subset_topspace disjnt_def inf.orderE inf_commute openin_closedin_eq)
+  moreover have "\<exists>U. openin X U \<and> S \<subseteq> U \<and> disjnt T (X closure_of U)"
+    if "\<And>U. openin X U \<and> S \<subseteq> U \<longrightarrow> (\<exists>V. openin X V \<and> S \<subseteq> V \<and> X closure_of V \<subseteq> U)"
+      and "closedin X S" "closedin X T" "disjnt S T"
+    for S T
+    using that   
+    by (smt (verit) Diff_Diff_Int Diff_eq_empty_iff Int_Diff closedin_def disjnt_def inf.absorb_iff2 inf.orderE)
+  ultimately show ?thesis
+    by (fastforce simp: normal_space)
+qed
+
+lemma normal_space_closures:
+   "normal_space X \<longleftrightarrow>
+    (\<forall>S T. S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and>
+              disjnt (X closure_of S) (X closure_of T)
+              \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V))" 
+   (is "?lhs=?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (meson closedin_closure_of closure_of_subset normal_space_def order.trans)
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (metis closedin_subset closure_of_eq normal_space_def)
+qed
+
+lemma normal_space_disjoint_closures:
+   "normal_space X \<longleftrightarrow>
+    (\<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T
+          \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and>
+                    disjnt (X closure_of U) (X closure_of V)))"
+   (is "?lhs=?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (metis closedin_closure_of normal_space)
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (smt (verit) closure_of_subset disjnt_iff normal_space openin_subset subset_eq)
+qed
+
+lemma normal_space_dual:
+   "normal_space X \<longleftrightarrow>
+    (\<forall>U V. openin X U \<longrightarrow> openin X V \<and> U \<union> V = topspace X
+          \<longrightarrow> (\<exists>S T. closedin X S \<and> closedin X T \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> S \<union> T = topspace X))"
+   (is "_ = ?rhs")
+proof -
+  have "normal_space X \<longleftrightarrow>
+        (\<forall>U V. closedin X U \<longrightarrow> closedin X V \<longrightarrow> disjnt U V \<longrightarrow>
+              (\<exists>S T. \<not> (openin X S \<and> openin X T \<longrightarrow>
+                         \<not> (U \<subseteq> S \<and> V \<subseteq> T \<and> disjnt S T))))"
+    unfolding normal_space_def by meson
+  also have "... \<longleftrightarrow> (\<forall>U V. openin X U \<longrightarrow> openin X V \<and> disjnt (topspace X - U) (topspace X - V) \<longrightarrow>
+              (\<exists>S T. \<not> (openin X S \<and> openin X T \<longrightarrow>
+                         \<not> (topspace X - U \<subseteq> S \<and> topspace X - V \<subseteq> T \<and> disjnt S T))))"
+    by (auto simp: all_closedin)
+  also have "... \<longleftrightarrow> ?rhs"
+  proof -
+    have *: "disjnt (topspace X - U) (topspace X - V) \<longleftrightarrow> U \<union> V = topspace X"
+      if "U \<subseteq> topspace X" "V \<subseteq> topspace X" for U V
+      using that by (auto simp: disjnt_iff)
+    show ?thesis
+      using ex_closedin *
+      apply (simp add: ex_closedin * [OF openin_subset openin_subset] cong: conj_cong)
+      apply (intro all_cong1 ex_cong1 imp_cong refl)
+      by (smt (verit, best) "*" Diff_Diff_Int Diff_subset Diff_subset_conv inf.orderE inf_commute openin_subset sup_commute)
+  qed
+  finally show ?thesis .
+qed
+
+
+lemma normal_t1_imp_Hausdorff_space:
+  assumes "normal_space X" "t1_space X"
+  shows "Hausdorff_space X"
+  unfolding Hausdorff_space_def
+proof clarify
+  fix x y
+  assume xy: "x \<in> topspace X" "y \<in> topspace X" "x \<noteq> y"
+  then have "disjnt {x} {y}"
+    by (auto simp: disjnt_iff)
+  then show "\<exists>U V. openin X U \<and> openin X V \<and> x \<in> U \<and> y \<in> V \<and> disjnt U V"
+    using assms xy closedin_t1_singleton normal_space_def
+    by (metis singletonI subsetD)
+qed
+
+lemma normal_t1_eq_Hausdorff_space:
+   "normal_space X \<Longrightarrow> t1_space X \<longleftrightarrow> Hausdorff_space X"
+  using normal_t1_imp_Hausdorff_space t1_or_Hausdorff_space by blast
+
+lemma normal_t1_imp_regular_space:
+   "\<lbrakk>normal_space X; t1_space X\<rbrakk> \<Longrightarrow> regular_space X"
+  by (metis compactin_imp_closedin normal_space_def normal_t1_eq_Hausdorff_space regular_space_compact_closed_sets)
+
+lemma compact_Hausdorff_or_regular_imp_normal_space:
+   "\<lbrakk>compact_space X; Hausdorff_space X \<or> regular_space X\<rbrakk>
+        \<Longrightarrow> normal_space X"
+  by (metis Hausdorff_space_compact_sets closedin_compact_space normal_space_def regular_space_compact_closed_sets)
+
+lemma normal_space_discrete_topology:
+   "normal_space(discrete_topology U)"
+  by (metis discrete_topology_closure_of inf_le2 normal_space_alt)
+
+lemma normal_space_fsigmas:
+  "normal_space X \<longleftrightarrow>
+    (\<forall>S T. fsigma_in X S \<and> fsigma_in X T \<and> separatedin X S T
+           \<longrightarrow> (\<exists>U B. openin X U \<and> openin X B \<and> S \<subseteq> U \<and> T \<subseteq> B \<and> disjnt U B))" (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  show ?rhs
+  proof clarify
+    fix S T
+    assume "fsigma_in X S" 
+    then obtain C where C: "\<And>n. closedin X (C n)" "\<And>n. C n \<subseteq> C (Suc n)" "\<Union> (range C) = S"
+      by (meson fsigma_in_ascending)
+    assume "fsigma_in X T" 
+    then obtain D where D: "\<And>n. closedin X (D n)" "\<And>n. D n \<subseteq> D (Suc n)" "\<Union> (range D) = T"
+      by (meson fsigma_in_ascending)
+    assume "separatedin X S T"
+    have "\<And>n. disjnt (D n) (X closure_of S)"
+      by (metis D(3) \<open>separatedin X S T\<close> disjnt_Union1 disjnt_def rangeI separatedin_def)
+    then have "\<And>n. \<exists>V V'. openin X V \<and> openin X V' \<and> D n \<subseteq> V \<and> X closure_of S \<subseteq> V' \<and> disjnt V V'"
+      by (metis D(1) L closedin_closure_of normal_space_def)
+    then obtain V V' where V: "\<And>n. openin X (V n)" and "\<And>n. openin X (V' n)" "\<And>n. disjnt (V n) (V' n)"
+          and DV:  "\<And>n. D n \<subseteq> V n" 
+          and subV': "\<And>n. X closure_of S \<subseteq> V' n"
+      by metis
+    then have VV: "V' n \<inter> X closure_of V n = {}" for n
+      using openin_Int_closure_of_eq_empty [of X "V' n" "V n"] by (simp add: Int_commute disjnt_def)
+    have "\<And>n. disjnt (C n) (X closure_of T)"
+      by (metis C(3) \<open>separatedin X S T\<close> disjnt_Union1 disjnt_def rangeI separatedin_def)
+    then have "\<And>n. \<exists>U U'. openin X U \<and> openin X U' \<and> C n \<subseteq> U \<and> X closure_of T \<subseteq> U' \<and> disjnt U U'"
+      by (metis C(1) L closedin_closure_of normal_space_def)
+    then obtain U U' where U: "\<And>n. openin X (U n)" and "\<And>n. openin X (U' n)" "\<And>n. disjnt (U n) (U' n)"
+          and CU:  "\<And>n. C n \<subseteq> U n" 
+          and subU': "\<And>n. X closure_of T \<subseteq> U' n"
+      by metis
+    then have UU: "U' n \<inter> X closure_of U n = {}" for n
+      using openin_Int_closure_of_eq_empty [of X "U' n" "U n"] by (simp add: Int_commute disjnt_def)
+    show "\<exists>U B. openin X U \<and> openin X B \<and> S \<subseteq> U \<and> T \<subseteq> B \<and> disjnt U B"
+    proof (intro conjI exI)
+      have "\<And>S n. closedin X (\<Union>m\<le>n. X closure_of V m)"
+        by (force intro: closedin_Union)
+      then show "openin X (\<Union>n. U n - (\<Union>m\<le>n. X closure_of V m))"
+        using U by blast
+      have "\<And>S n. closedin X (\<Union>m\<le>n. X closure_of U m)"
+        by (force intro: closedin_Union)
+      then show "openin X (\<Union>n. V n - (\<Union>m\<le>n. X closure_of U m))"
+        using V by blast
+      have "S \<subseteq> topspace X"
+        by (simp add: \<open>fsigma_in X S\<close> fsigma_in_subset)
+      then show "S \<subseteq> (\<Union>n. U n - (\<Union>m\<le>n. X closure_of V m))"
+        apply (clarsimp simp: Ball_def)
+        by (metis VV C(3) CU IntI UN_E closure_of_subset empty_iff subV' subsetD)
+      have "T \<subseteq> topspace X"
+        by (simp add: \<open>fsigma_in X T\<close> fsigma_in_subset)
+      then show "T \<subseteq> (\<Union>n. V n - (\<Union>m\<le>n. X closure_of U m))"
+        apply (clarsimp simp: Ball_def)
+        by (metis UU D(3) DV IntI UN_E closure_of_subset empty_iff subU' subsetD)
+      have "\<And>x m n. \<lbrakk>x \<in> U n; x \<in> V m; \<forall>k\<le>m. x \<notin> X closure_of U k\<rbrakk> \<Longrightarrow> \<exists>k\<le>n. x \<in> X closure_of V k"
+        by (meson U V closure_of_subset nat_le_linear openin_subset subsetD)
+      then show "disjnt (\<Union>n. U n - (\<Union>m\<le>n. X closure_of V m)) (\<Union>n. V n - (\<Union>m\<le>n. X closure_of U m))"
+        by (force simp: disjnt_iff)
+    qed
+  qed
+next
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (simp add: closed_imp_fsigma_in normal_space_def separatedin_closed_sets)
+qed
+
+lemma normal_space_fsigma_subtopology:
+  assumes "normal_space X" "fsigma_in X S"
+  shows "normal_space (subtopology X S)"
+  unfolding normal_space_fsigmas
+proof clarify
+  fix T U
+  assume "fsigma_in (subtopology X S) T"
+      and "fsigma_in (subtopology X S) U"
+      and TU: "separatedin (subtopology X S) T U"
+  then obtain A B where "openin X A \<and> openin X B \<and> T \<subseteq> A \<and> U \<subseteq> B \<and> disjnt A B"
+    by (metis assms fsigma_in_fsigma_subtopology normal_space_fsigmas separatedin_subtopology)
+  then
+  show "\<exists>A B. openin (subtopology X S) A \<and> openin (subtopology X S) B \<and> T \<subseteq> A \<and>
+   U \<subseteq> B \<and> disjnt A B"
+    using TU
+    by (force simp add: separatedin_subtopology openin_subtopology_alt disjnt_iff)
+qed
+
+lemma normal_space_closed_subtopology:
+  assumes "normal_space X" "closedin X S"
+  shows "normal_space (subtopology X S)"
+  by (simp add: assms closed_imp_fsigma_in normal_space_fsigma_subtopology)
+
+lemma normal_space_continuous_closed_map_image:
+  assumes "normal_space X" and contf: "continuous_map X Y f" 
+    and clof: "closed_map X Y f"  and fim: "f ` topspace X = topspace Y"
+shows "normal_space Y"
+  unfolding normal_space_def
+proof clarify
+  fix S T
+  assume "closedin Y S" and "closedin Y T" and "disjnt S T"
+  have "closedin X {x \<in> topspace X. f x \<in> S}" "closedin X {x \<in> topspace X. f x \<in> T}"
+    using \<open>closedin Y S\<close> \<open>closedin Y T\<close> closedin_continuous_map_preimage contf by auto
+  moreover
+  have "disjnt {x \<in> topspace X. f x \<in> S} {x \<in> topspace X. f x \<in> T}"
+    using \<open>disjnt S T\<close> by (auto simp: disjnt_iff)
+  ultimately
+  obtain U V where "closedin X U" "closedin X V" 
+    and subXU: "{x \<in> topspace X. f x \<in> S} \<subseteq> topspace X - U" 
+    and subXV: "{x \<in> topspace X. f x \<in> T} \<subseteq> topspace X - V" 
+    and dis: "disjnt (topspace X - U) (topspace X -V)"
+    using \<open>normal_space X\<close> by (force simp add: normal_space_def ex_openin)
+  have "closedin Y (f ` U)" "closedin Y (f ` V)"
+    using \<open>closedin X U\<close> \<open>closedin X V\<close> clof closed_map_def by blast+
+  moreover have "S \<subseteq> topspace Y - f ` U"
+    using \<open>closedin Y S\<close> \<open>closedin X U\<close> subXU by (force dest: closedin_subset)
+  moreover have "T \<subseteq> topspace Y - f ` V"
+    using \<open>closedin Y T\<close> \<open>closedin X V\<close> subXV by (force dest: closedin_subset)
+  moreover have "disjnt (topspace Y - f ` U) (topspace Y - f ` V)"
+    using fim dis by (force simp add: disjnt_iff)
+  ultimately show "\<exists>U V. openin Y U \<and> openin Y V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
+    by (force simp add: ex_openin)
+qed
+
+
+subsection \<open>Hereditary topological properties\<close>
+
+definition hereditarily 
+  where "hereditarily P X \<equiv>
+        \<forall>S. S \<subseteq> topspace X \<longrightarrow> P(subtopology X S)"
+
+lemma hereditarily:
+   "hereditarily P X \<longleftrightarrow> (\<forall>S. P(subtopology X S))"
+  by (metis Int_lower1 hereditarily_def subtopology_restrict)
+
+lemma hereditarily_mono:
+   "\<lbrakk>hereditarily P X; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> hereditarily Q X"
+  by (simp add: hereditarily)
+
+lemma hereditarily_inc:
+   "hereditarily P X \<Longrightarrow> P X"
+  by (metis hereditarily subtopology_topspace)
+
+lemma hereditarily_subtopology:
+   "hereditarily P X \<Longrightarrow> hereditarily P (subtopology X S)"
+  by (simp add: hereditarily subtopology_subtopology)
+
+lemma hereditarily_normal_space_continuous_closed_map_image:
+  assumes X: "hereditarily normal_space X" and contf: "continuous_map X Y f" 
+    and clof: "closed_map X Y f"  and fim: "f ` (topspace X) = topspace Y" 
+  shows "hereditarily normal_space Y"
+  unfolding hereditarily_def
+proof (intro strip)
+  fix T
+  assume "T \<subseteq> topspace Y"
+  then have nx: "normal_space (subtopology X {x \<in> topspace X. f x \<in> T})"
+    by (meson X hereditarily)
+  moreover have "continuous_map (subtopology X {x \<in> topspace X. f x \<in> T}) (subtopology Y T) f"
+    by (simp add: contf continuous_map_from_subtopology continuous_map_in_subtopology image_subset_iff)
+  moreover have "closed_map (subtopology X {x \<in> topspace X. f x \<in> T}) (subtopology Y T) f"
+    by (simp add: clof closed_map_restriction)
+  ultimately show "normal_space (subtopology Y T)"
+    using fim normal_space_continuous_closed_map_image by fastforce
+qed
+
+lemma homeomorphic_hereditarily_normal_space:
+   "X homeomorphic_space Y
+      \<Longrightarrow> (hereditarily normal_space X \<longleftrightarrow> hereditarily normal_space Y)"
+  by (meson hereditarily_normal_space_continuous_closed_map_image homeomorphic_eq_everything_map 
+      homeomorphic_space homeomorphic_space_sym)
+
+lemma hereditarily_normal_space_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; hereditarily normal_space X\<rbrakk> \<Longrightarrow> hereditarily normal_space Y"
+  by (smt (verit) hereditarily_subtopology hereditary_imp_retractive_property homeomorphic_hereditarily_normal_space)
+
+subsection\<open>Limits in a topological space\<close>
+
+lemma limitin_const_iff:
+  assumes "t1_space X" "\<not> trivial_limit F"
+  shows "limitin X (\<lambda>k. a) l F \<longleftrightarrow> l \<in> topspace X \<and> a = l"  (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    using assms unfolding limitin_def t1_space_def by (metis eventually_const openin_topspace)
+next
+  assume ?rhs then show ?lhs
+    using assms by (auto simp: limitin_def t1_space_def)
+qed
+
+lemma compactin_sequence_with_limit:
+  assumes lim: "limitin X \<sigma> l sequentially" and "S \<subseteq> range \<sigma>" and SX: "S \<subseteq> topspace X"
+  shows "compactin X (insert l S)"
+unfolding compactin_def
+proof (intro conjI strip)
+  show "insert l S \<subseteq> topspace X"
+    by (meson SX insert_subset lim limitin_topspace)
+  fix \<U>
+  assume \<section>: "Ball \<U> (openin X) \<and> insert l S \<subseteq> \<Union> \<U>"
+  have "\<exists>V. finite V \<and> V \<subseteq> \<U> \<and> (\<exists>t \<in> V. l \<in> t) \<and> S \<subseteq> \<Union> V"
+    if *: "\<forall>x \<in> S. \<exists>T \<in> \<U>. x \<in> T" and "T \<in> \<U>" "l \<in> T" for T
+  proof -
+    obtain V where V: "\<And>x. x \<in> S \<Longrightarrow> V x \<in> \<U> \<and> x \<in> V x"
+      using * by metis
+    obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> \<sigma> n \<in> T"
+      by (meson "\<section>" \<open>T \<in> \<U>\<close> \<open>l \<in> T\<close> lim limitin_sequentially)
+    show ?thesis
+    proof (intro conjI exI)
+      have "x \<in> T"
+        if "x \<in> S" and "\<forall>A. (\<forall>x \<in> S. (\<forall>n\<le>N. x \<noteq> \<sigma> n) \<or> A \<noteq> V x) \<or> x \<notin> A" for x 
+        by (metis (no_types) N V that assms(2) imageE nle_le subsetD)
+      then show "S \<subseteq> \<Union> (insert T (V ` (S \<inter> \<sigma> ` {0..N})))"
+        by force
+    qed (use V that in auto)
+  qed
+  then show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> insert l S \<subseteq> \<Union> \<F>"
+    by (smt (verit, best) Union_iff \<section> insert_subset subsetD)
+qed
+
+lemma limitin_Hausdorff_unique:
+  assumes "limitin X f l1 F" "limitin X f l2 F" "\<not> trivial_limit F" "Hausdorff_space X"
+  shows "l1 = l2"
+proof (rule ccontr)
+  assume "l1 \<noteq> l2"
+  with assms obtain U V where "openin X U" "openin X V" "l1 \<in> U" "l2 \<in> V" "disjnt U V"
+    by (metis Hausdorff_space_def limitin_topspace)
+  then have "eventually (\<lambda>x. f x \<in> U) F" "eventually (\<lambda>x. f x \<in> V) F"
+    using assms by (fastforce simp: limitin_def)+
+  then have "\<exists>x. f x \<in> U \<and> f x \<in> V"
+    using assms eventually_elim2 filter_eq_iff by fastforce
+  with assms \<open>disjnt U V\<close> show False
+    by (meson disjnt_iff)
+qed
+
+lemma limitin_kc_unique:
+  assumes "kc_space X" and lim1: "limitin X f l1 sequentially" and lim2: "limitin X f l2 sequentially"
+  shows "l1 = l2"
+proof (rule ccontr)
+  assume "l1 \<noteq> l2"
+  define A where "A \<equiv> insert l1 (range f - {l2})"
+  have "l1 \<in> topspace X"
+    using lim1 limitin_def by fastforce
+  moreover have "compactin X (insert l1 (topspace X \<inter> (range f - {l2})))"
+    by (meson Diff_subset compactin_sequence_with_limit inf_le1 inf_le2 lim1 subset_trans)
+  ultimately have "compactin X (topspace X \<inter> A)"
+    by (simp add: A_def)
+  then have OXA: "openin X (topspace X - A)"
+    by (metis Diff_Diff_Int Diff_subset \<open>kc_space X\<close> kc_space_def openin_closedin_eq)
+  have "l2 \<in> topspace X - A"
+    using \<open>l1 \<noteq> l2\<close> A_def lim2 limitin_topspace by fastforce
+  then have "\<forall>\<^sub>F x in sequentially. f x = l2"
+    using limitinD [OF lim2 OXA] by (auto simp: A_def eventually_conj_iff)
+  then show False
+    using limitin_transform_eventually [OF _ lim1] 
+          limitin_const_iff [OF kc_imp_t1_space trivial_limit_sequentially]
+    using \<open>l1 \<noteq> l2\<close> \<open>kc_space X\<close> by fastforce
+qed
+
+lemma limitin_closedin:
+  assumes lim: "limitin X f l F" 
+    and "closedin X S" and ev: "eventually (\<lambda>x. f x \<in> S) F" "\<not> trivial_limit F"
+  shows "l \<in> S"
+proof (rule ccontr)
+  assume "l \<notin> S"
+  have "\<forall>\<^sub>F x in F. f x \<in> topspace X - S"
+    by (metis Diff_iff \<open>l \<notin> S\<close> \<open>closedin X S\<close> closedin_def lim limitin_def)
+  with ev eventually_elim2 trivial_limit_def show False
+    by force
+qed
+
 end
 
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Sun May 07 14:52:53 2023 +0100
@@ -383,6 +383,10 @@
      "closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
   by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)
 
+lemma closedin_trans_full:
+   "\<lbrakk>closedin (subtopology X U) S; closedin X U\<rbrakk> \<Longrightarrow> closedin X S"
+  using closedin_closed_subtopology by blast
+
 lemma openin_subtopology_Un:
     "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
      \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
@@ -4038,6 +4042,7 @@
   shows "continuous_map euclidean (top_of_set S) f"
   by (simp add: cont continuous_map_into_subtopology eq image_subset_iff_subset_vimage)
 
+
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Half-global and completely global cases\<close>
 
 lemma continuous_openin_preimage_gen:
@@ -4481,6 +4486,188 @@
   using assms continuous_on_generated_topo_iff by blast
 
 
+subsection\<open>Continuity via bases/subbases, hence upper and lower semicontinuity\<close>
+
+lemma continuous_map_into_topology_base:
+  assumes P: "openin Y = arbitrary union_of P"
+    and f: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
+    and ope: "\<And>U. P U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
+  shows "continuous_map X Y f"
+proof -
+  have *: "\<And>\<U>. (\<And>t. t \<in> \<U> \<Longrightarrow> P t) \<Longrightarrow> openin X {x \<in> topspace X. \<exists>U\<in>\<U>. f x \<in> U}"
+    by (smt (verit) Ball_Collect ope mem_Collect_eq openin_subopen)
+  show ?thesis
+    using P by (auto simp: continuous_map_def arbitrary_def union_of_def intro!: f *)
+qed
+
+lemma continuous_map_into_topology_base_eq:
+  assumes P: "openin Y = arbitrary union_of P"
+  shows
+   "continuous_map X Y f \<longleftrightarrow>
+    (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and> (\<forall>U. P U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
+ (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  then have "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
+    by (meson continuous_map_def)
+  moreover have "\<And>U. P U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
+    using L assms continuous_map openin_topology_base_unique by fastforce
+  ultimately show ?rhs by auto
+qed (simp add: assms continuous_map_into_topology_base)
+
+lemma continuous_map_into_topology_subbase:
+  fixes U P
+  defines "Y \<equiv> topology(arbitrary union_of (finite intersection_of P relative_to U))"
+  assumes f: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
+    and ope: "\<And>U. P U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
+  shows "continuous_map X Y f"
+proof (intro continuous_map_into_topology_base)
+  show "openin Y = arbitrary union_of (finite intersection_of P relative_to U)"
+    unfolding Y_def using istopology_subbase topology_inverse' by blast
+  show "openin X {x \<in> topspace X. f x \<in> V}"
+    if \<section>: "(finite intersection_of P relative_to U) V" for V 
+  proof -
+    define finv where "finv \<equiv> \<lambda>V. {x \<in> topspace X. f x \<in> V}"
+    obtain \<U> where \<U>: "finite \<U>" "\<And>V. V \<in> \<U> \<Longrightarrow> P V"
+                      "{x \<in> topspace X. f x \<in> V} = (\<Inter>V \<in> insert U \<U>. finv V)"
+      using \<section> by (fastforce simp: finv_def intersection_of_def relative_to_def)
+    show ?thesis
+      unfolding \<U>
+    proof (intro openin_Inter ope)
+      have U: "U = topspace Y"
+        unfolding Y_def using topspace_subbase by fastforce
+      fix V
+      assume V: "V \<in> finv ` insert U \<U>"
+      with U f have "openin X {x \<in> topspace X. f x \<in> U}"
+        by (auto simp: openin_subopen [of X "Collect _"])
+      then show "openin X V"
+        using V \<U>(2) ope by (fastforce simp: finv_def)
+    qed (use \<open>finite \<U>\<close> in auto)
+  qed
+qed (use f in auto)
+
+lemma continuous_map_into_topology_subbase_eq:
+  assumes "Y = topology(arbitrary union_of (finite intersection_of P relative_to U))"
+  shows
+   "continuous_map X Y f \<longleftrightarrow>
+    (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and> (\<forall>U. P U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
+   (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  show ?rhs
+  proof (intro conjI strip)
+    show "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
+      using L continuous_map_def by fastforce
+    fix V
+    assume "P V"
+    have "U = topspace Y"
+      unfolding assms using topspace_subbase by fastforce
+    then have eq: "{x \<in> topspace X. f x \<in> V} = {x \<in> topspace X. f x \<in> U \<inter> V}"
+      using L by (auto simp: continuous_map)
+    have "openin Y (U \<inter> V)"
+      unfolding assms openin_subbase
+      by (meson \<open>P V\<close> arbitrary_union_of_inc finite_intersection_of_inc relative_to_inc)
+    show "openin X {x \<in> topspace X. f x \<in> V}"
+      using L \<open>openin Y (U \<inter> V)\<close> continuous_map eq by fastforce
+  qed
+next
+  show "?rhs \<Longrightarrow> ?lhs"
+    unfolding assms
+    by (intro continuous_map_into_topology_subbase) auto
+qed 
+
+lemma subbase_subtopology_euclidean:
+  fixes U :: "'a::order_topology set"
+  shows
+  "topology
+    (arbitrary union_of
+      (finite intersection_of (\<lambda>x. x \<in> range greaterThan \<union> range lessThan) relative_to U))
+ = subtopology euclidean U"
+proof -
+  have "\<exists>V. (finite intersection_of (\<lambda>x. x \<in> range greaterThan \<or> x \<in> range lessThan)) V \<and> x \<in> V \<and> V \<subseteq> W"
+    if "open W" "x \<in> W" for W and x::'a
+    using \<open>open W\<close> [unfolded open_generated_order] \<open>x \<in> W\<close>
+  proof (induct rule: generate_topology.induct)
+    case UNIV
+    then show ?case
+      using finite_intersection_of_empty by blast
+  next
+    case (Int a b)
+    then show ?case 
+        by (meson Int_iff finite_intersection_of_Int inf_mono)
+  next
+    case (UN K)
+    then show ?case
+      by (meson Union_iff subset_iff)
+  next
+    case (Basis s)
+    then show ?case
+      by (metis (no_types, lifting) Un_iff finite_intersection_of_inc order_refl)
+  qed
+  moreover 
+  have "\<And>V::'a set. (finite intersection_of (\<lambda>x. x \<in> range greaterThan \<or> x \<in> range lessThan)) V \<Longrightarrow> open V"
+    by (force simp: intersection_of_def subset_iff)
+  ultimately have *: "openin (euclidean::'a topology) = 
+           (arbitrary union_of (finite intersection_of (\<lambda>x. x \<in> range greaterThan \<or> x \<in> range lessThan)))" 
+    by (smt (verit, best) openin_topology_base_unique open_openin)
+  show ?thesis
+    unfolding subtopology_def arbitrary_union_of_relative_to [symmetric] 
+    apply (simp add: relative_to_def flip: *)
+    by (metis Int_commute)
+qed
+
+lemma continuous_map_upper_lower_semicontinuous_lt_gen:
+  fixes U :: "'a::order_topology set"
+  shows "continuous_map X (subtopology euclidean U) f \<longleftrightarrow>
+         (\<forall>x \<in> topspace X. f x \<in> U) \<and>
+         (\<forall>a. openin X {x \<in> topspace X. f x > a}) \<and>
+         (\<forall>a. openin X {x \<in> topspace X. f x < a})"
+  by (auto simp: continuous_map_into_topology_subbase_eq [OF subbase_subtopology_euclidean [symmetric, of U]] 
+           greaterThan_def lessThan_def image_iff   simp flip: all_simps)
+
+lemma continuous_map_upper_lower_semicontinuous_lt:
+  fixes f :: "'a \<Rightarrow> 'b::order_topology"
+  shows "continuous_map X euclidean f \<longleftrightarrow>
+         (\<forall>a. openin X {x \<in> topspace X. f x > a}) \<and>
+         (\<forall>a. openin X {x \<in> topspace X. f x < a})"
+  using continuous_map_upper_lower_semicontinuous_lt_gen [where U=UNIV]
+  by auto
+
+lemma Int_Collect_imp_eq: "A \<inter> {x. x\<in>A \<longrightarrow> P x} = {x\<in>A. P x}"
+  by blast
+
+lemma continuous_map_upper_lower_semicontinuous_le_gen:
+  shows
+    "continuous_map X (subtopology euclideanreal U) f \<longleftrightarrow>
+         (\<forall>x \<in> topspace X. f x \<in> U) \<and>
+         (\<forall>a. closedin X {x \<in> topspace X. f x \<ge> a}) \<and>
+         (\<forall>a. closedin X {x \<in> topspace X. f x \<le> a})"
+  unfolding continuous_map_upper_lower_semicontinuous_lt_gen
+  by (auto simp: closedin_def Diff_eq Compl_eq not_le Int_Collect_imp_eq)
+
+lemma continuous_map_upper_lower_semicontinuous_le:
+   "continuous_map X euclideanreal f \<longleftrightarrow>
+         (\<forall>a. closedin X {x \<in> topspace X. f x \<ge> a}) \<and>
+         (\<forall>a. closedin X {x \<in> topspace X. f x \<le> a})"
+  using continuous_map_upper_lower_semicontinuous_le_gen [where U=UNIV]
+  by auto
+
+lemma continuous_map_upper_lower_semicontinuous_lte_gen:
+   "continuous_map X (subtopology euclideanreal U) f \<longleftrightarrow>
+         (\<forall>x \<in> topspace X. f x \<in> U) \<and>
+         (\<forall>a. openin X {x \<in> topspace X. f x < a}) \<and>
+         (\<forall>a. closedin X {x \<in> topspace X. f x \<le> a})"
+  unfolding continuous_map_upper_lower_semicontinuous_lt_gen
+  by (auto simp: closedin_def Diff_eq Compl_eq not_le Int_Collect_imp_eq)
+
+lemma continuous_map_upper_lower_semicontinuous_lte:
+   "continuous_map X euclideanreal f \<longleftrightarrow>
+         (\<forall>a. openin X {x \<in> topspace X. f x < a}) \<and>
+         (\<forall>a. closedin X {x \<in> topspace X. f x \<le> a})"
+  using continuous_map_upper_lower_semicontinuous_lte_gen [where U=UNIV]
+  by auto
+
+
 subsection\<^marker>\<open>tag important\<close> \<open>Pullback topology\<close>
 
 text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Sun May 07 14:52:53 2023 +0100
@@ -347,7 +347,7 @@
       continuous_on S f; continuous_on T f\<rbrakk>
      \<Longrightarrow> continuous_on (S \<union> T) f"
   unfolding continuous_on closedin_limpt
-  by (metis Lim_trivial_limit Lim_within_union Un_iff trivial_limit_within)
+  by (metis Lim_trivial_limit Lim_within_Un Un_iff trivial_limit_within)
 
 lemma continuous_on_cases_local:
      "\<lbrakk>closedin (top_of_set (S \<union> T)) S; closedin (top_of_set (S \<union> T)) T;
@@ -1612,4 +1612,31 @@
     connected_component_of_set X x = connected_component_of_set X y"
   by (meson connected_component_of_nonoverlap)
 
+subsection\<open>Combining theorems for continuous functions into the reals\<close>
+
+text \<open>The homeomorphism between the real line and the open interval $(-1,1)$\<close>
+
+lemma continuous_map_real_shrink:
+  "continuous_map euclideanreal (top_of_set {-1<..<1}) (\<lambda>x. x / (1 + \<bar>x\<bar>))"
+proof -
+  have "continuous_on UNIV (\<lambda>x::real. x / (1 + \<bar>x\<bar>))"
+    by (intro continuous_intros) auto
+  then show ?thesis
+    by (auto simp: continuous_map_in_subtopology divide_simps)
+qed
+
+lemma continuous_on_real_grow:
+  "continuous_on {-1<..<1} (\<lambda>x::real. x / (1 - \<bar>x\<bar>))"
+  by (intro continuous_intros) auto
+
+lemma real_grow_shrink:
+  fixes x::real 
+  shows "x / (1 + \<bar>x\<bar>) / (1 - \<bar>x / (1 + \<bar>x\<bar>)\<bar>) = x"
+  by (force simp: divide_simps)
+
+lemma homeomorphic_maps_real_shrink:
+  "homeomorphic_maps euclideanreal (subtopology euclideanreal {-1<..<1}) 
+     (\<lambda>x. x / (1 + \<bar>x\<bar>))  (\<lambda>y. y / (1 - \<bar>y\<bar>))"
+  by (force simp: homeomorphic_maps_def continuous_map_real_shrink continuous_on_real_grow divide_simps)
+
 end
\ No newline at end of file
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Analysis/Arcwise_Connected.thy
--- a/src/HOL/Analysis/Arcwise_Connected.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Sun May 07 14:52:53 2023 +0100
@@ -533,6 +533,216 @@
   by (auto simp: field_split_simps)
 
 
+lemma padic_rational_approximation_straddle:
+  assumes "\<epsilon> > 0" "p > 1"
+  obtains n q r 
+    where "of_int q / p^n < x" "x < of_int r / p^n" "\<bar>q / p^n - r / p^n \<bar> < \<epsilon>"
+proof -
+  obtain n where n: "2 / \<epsilon> < p ^ n"
+    using \<open>p>1\<close> real_arch_pow by blast
+  define q where "q \<equiv> \<lfloor>p ^ n * x\<rfloor> - 1"
+  show thesis
+    proof
+      show "q / p ^ n < x" "x < real_of_int (q+2) / p ^ n"
+        using assms by (simp_all add: q_def divide_simps floor_less_cancel mult.commute)
+      show "\<bar>q / p ^ n - real_of_int (q+2) / p ^ n\<bar> < \<epsilon>"
+        using assms n by (simp add: q_def divide_simps mult.commute)
+    qed
+qed
+
+lemma padic_rational_approximation_straddle_pos:
+  assumes "\<epsilon> > 0" "p > 1" "x > 0"
+  obtains n q r 
+    where "of_nat q / p^n < x" "x < of_nat r / p^n" "\<bar>q / p^n - r / p^n \<bar> < \<epsilon>"
+proof -
+  obtain n q r 
+    where *: "of_int q / p^n < x" "x < of_int r / p^n" "\<bar>q / p^n - r / p^n \<bar> < \<epsilon>"
+    using padic_rational_approximation_straddle assms by metis
+  then have "r \<ge> 0"
+    using assms by (smt (verit, best) divide_nonpos_pos of_int_0_le_iff zero_less_power)
+  show thesis
+  proof
+    show "real (max 0 (nat q)) / p ^ n < x"
+      using * by (metis assms(3) div_0 max_nat.left_neutral nat_eq_iff2 of_nat_0 of_nat_nat) 
+    show "x < real (nat r) / p ^ n"
+      using \<open>r \<ge> 0\<close> * by force
+    show "\<bar>real (max 0 (nat q)) / p ^ n - real (nat r) / p ^ n\<bar> < \<epsilon>"
+      using * assms by (simp add: divide_simps)
+  qed
+qed
+
+lemma padic_rational_approximation_straddle_pos_le:
+  assumes "\<epsilon> > 0" "p > 1" "x \<ge> 0"
+  obtains n q r 
+    where "of_nat q / p^n \<le> x" "x < of_nat r / p^n" "\<bar>q / p^n - r / p^n \<bar> < \<epsilon>"
+proof -
+  obtain n q r 
+    where *: "of_int q / p^n < x" "x < of_int r / p^n" "\<bar>q / p^n - r / p^n \<bar> < \<epsilon>"
+    using padic_rational_approximation_straddle assms by metis
+  then have "r \<ge> 0"
+    using assms by (smt (verit, best) divide_nonpos_pos of_int_0_le_iff zero_less_power)
+  show thesis
+  proof
+    show "real (max 0 (nat q)) / p ^ n \<le> x"
+      using * assms(3) nle_le by fastforce
+    show "x < real (nat r) / p ^ n"
+      using \<open>r \<ge> 0\<close> * by force
+    show "\<bar>real (max 0 (nat q)) / p ^ n - real (nat r) / p ^ n\<bar> < \<epsilon>"
+       using * assms by (simp add: divide_simps)
+  qed
+qed
+
+
+subsubsection \<open>Definition by recursion on dyadic rationals in [0,1]\<close>
+
+lemma recursion_on_dyadic_fractions:
+  assumes base: "R a b"
+    and step: "\<And>x y. R x y \<Longrightarrow> \<exists>z. R x z \<and> R z y" and trans: "\<And>x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z"
+  shows "\<exists>f :: real \<Rightarrow> 'a. f 0 = a \<and> f 1 = b \<and>
+               (\<forall>x \<in> dyadics \<inter> {0..1}. \<forall>y \<in> dyadics \<inter> {0..1}. x < y \<longrightarrow> R (f x) (f y))"
+proof -
+  obtain mid where mid: "R x y \<Longrightarrow> R x (mid x y)" "R x y \<Longrightarrow> R (mid x y) y" for x y 
+    using step by metis
+  define g where "g \<equiv> rec_nat (\<lambda>k. if k = 0 then a else b) (\<lambda>n r k. if even k then r (k div 2) else mid (r ((k - 1) div 2)) (r ((Suc k) div 2)))"
+  have g0 [simp]: "g 0 = (\<lambda>k. if k = 0 then a else b)"
+    by (simp add: g_def)
+  have gSuc [simp]: "\<And>n. g(Suc n) = (\<lambda>k. if even k then g n (k div 2) else mid (g n ((k - 1) div 2)) (g n ((Suc k) div 2)))"
+    by (auto simp: g_def)
+  have g_eq_g: "2 ^ d * k = k' \<Longrightarrow> g n k = g (n + d) k'" for n d k k'
+    by (induction d arbitrary: k k') auto
+  have "g n k = g n' k'" if "real k / 2^n = real k' / 2^n'" "n' \<le> n" for k n k' n'
+  proof -
+    have "real k = real k' * 2 ^ (n-n')"
+      using that by (simp add: power_diff divide_simps)
+    then have "k = k' * 2 ^ (n-n')"
+      using of_nat_eq_iff by fastforce
+    with g_eq_g show ?thesis
+      by (metis le_add_diff_inverse mult.commute that(2))
+  qed
+  then have g_eq_g: "g n k = g n' k'" if "real k / 2 ^ n = real k' / 2 ^ n'" for k n k' n'
+    by (metis nat_le_linear that)
+  then obtain f where "(\<lambda>(k,n). g n k) = f \<circ> (\<lambda>(k,n). k / 2 ^ n)"
+    using function_factors_left by (smt (verit, del_insts) case_prod_beta')
+  then have f_eq_g: "\<And>k n. f(real k / 2 ^ n) = g n k"
+    by (simp add: fun_eq_iff)
+  show ?thesis
+  proof (intro exI conjI strip)
+    show "f 0 = a"
+      by (metis f_eq_g g0 div_0 of_nat_0)
+    show "f 1 = b"
+      by (metis f_eq_g g0 div_by_1 of_nat_1_eq_iff power_0 zero_neq_one)
+    show "R (f x) (f y)" 
+      if x: "x \<in> dyadics \<inter> {0..1}" and y: "y \<in> dyadics \<inter> {0..1}" and "x < y" for x y
+    proof -
+      obtain n1 k1 where xeq: "x = real k1 / 2^n1" "k1 \<le> 2^n1"
+        using x by (auto simp: dyadics_def)
+      obtain n2 k2 where yeq: "y = real k2 / 2^n2" "k2 \<le> 2^n2"
+        using y by (auto simp: dyadics_def)
+      have xcommon: "x = real(2^n2 * k1) / 2 ^ (n1+n2)"
+        using xeq by (simp add: power_add)
+      have ycommon: "y = real(2^n1 * k2) / 2 ^ (n1+n2)"
+        using yeq by (simp add: power_add)
+      have *: "R (g n j) (g n k)" if "j < k" "k \<le> 2^n" for n j k
+        using that
+      proof (induction n arbitrary: j k)
+        case 0
+        then show ?case
+          by (simp add: base)
+      next
+        case (Suc n)
+        show ?case
+        proof (cases "even j")
+          case True
+          then obtain a where [simp]: "j = 2*a"
+            by blast
+          show ?thesis 
+          proof (cases "even k")
+            case True
+            with Suc show ?thesis
+              by (auto elim!: evenE)
+          next
+            case False
+            then obtain b where [simp]: "k = Suc (2*b)"
+              using oddE by fastforce
+            show ?thesis
+              using Suc
+              apply simp
+              by (smt (verit, ccfv_SIG) less_Suc_eq linorder_not_le local.trans mid(1) nat_mult_less_cancel1 pos2)
+          qed
+        next
+          case False
+          then obtain a where [simp]: "j = Suc (2*a)"
+            using oddE by fastforce
+          show ?thesis
+          proof (cases "even k")
+            case True
+            then obtain b where [simp]: "k = 2*b"
+              by blast
+            show ?thesis
+              using Suc 
+              apply simp
+              by (smt (verit, ccfv_SIG) Suc_leI Suc_lessD le_trans lessI linorder_neqE_nat linorder_not_le local.trans mid(2) nat_mult_less_cancel1 pos2)
+          next
+            case False
+            then obtain b where [simp]: "k = Suc (2*b)"
+              using oddE by fastforce
+            show ?thesis
+              using Suc 
+              apply simp
+              by (smt (verit) Suc_leI le_trans lessI less_or_eq_imp_le linorder_neqE_nat linorder_not_le local.trans mid(1) mid(2) nat_mult_less_cancel1 pos2)
+            qed
+        qed
+      qed
+      show ?thesis
+        unfolding xcommon ycommon f_eq_g
+      proof (rule *)
+        show "2 ^ n2 * k1 < 2 ^ n1 * k2"
+          using of_nat_less_iff \<open>x < y\<close> by (fastforce simp: xeq yeq field_simps)
+        show "2 ^ n1 * k2 \<le> 2 ^ (n1 + n2)"
+          by (simp add: power_add yeq)
+      qed
+    qed
+  qed
+qed
+
+lemma dyadics_add:
+  assumes "x \<in> dyadics" "y \<in> dyadics"
+  shows "x+y \<in> dyadics"
+proof -
+  obtain i j m n where x: "x = of_nat i / 2 ^ m" and y: "y = of_nat j / 2 ^ n"
+    using assms by (auto simp: dyadics_def)
+  have xcommon: "x = of_nat(2^n * i) / 2 ^ (m+n)"
+    using x by (simp add: power_add)
+  moreover
+  have ycommon: "y = of_nat(2^m * j) / 2 ^ (m+n)"
+    using y by (simp add: power_add)
+  ultimately have "x+y = (of_nat(2^n * i + 2^m * j)) / 2 ^ (m+n)"
+    by (simp add: field_simps)
+  then show ?thesis
+    unfolding dyadics_def by blast
+qed
+
+lemma dyadics_diff:
+  fixes x :: "'a::linordered_field"
+  assumes "x \<in> dyadics" "y \<in> dyadics" "y \<le> x"
+  shows "x-y \<in> dyadics"
+proof -
+  obtain i j m n where x: "x = of_nat i / 2 ^ m" and y: "y = of_nat j / 2 ^ n"
+    using assms by (auto simp: dyadics_def)
+  have j_le_i: "j * 2 ^ m \<le> i * 2 ^ n"
+    using of_nat_le_iff \<open>y \<le> x\<close> unfolding x y by (fastforce simp add: divide_simps)
+  have xcommon: "x = of_nat(2^n * i) / 2 ^ (m+n)"
+    using x by (simp add: power_add)
+  moreover
+  have ycommon: "y = of_nat(2^m * j) / 2 ^ (m+n)"
+    using y by (simp add: power_add)
+  ultimately have "x-y = (of_nat(2^n * i - 2^m * j)) / 2 ^ (m+n)"
+    by (simp add: xcommon ycommon field_simps j_le_i of_nat_diff)
+  then show ?thesis
+    unfolding dyadics_def by blast
+qed
+
+
 
 theorem homeomorphic_monotone_image_interval:
   fixes f :: "real \<Rightarrow> 'a::{real_normed_vector,complete_space}"
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun May 07 14:52:53 2023 +0100
@@ -175,39 +175,6 @@
   finally show "norm (A *v x) \<le> CARD('m) * real (CARD('n)) * B * norm x" .
 qed
 
-lemma rational_approximation:
-  assumes "e > 0"
-  obtains r::real where "r \<in> \<rat>" "\<bar>r - x\<bar> < e"
-  using Rats_dense_in_real [of "x - e/2" "x + e/2"] assms by auto
-
-lemma Rats_closure_real: "closure \<rat> = (UNIV::real set)"
-proof -
-  have "\<And>x::real. x \<in> closure \<rat>"
-    by (metis closure_approachable dist_real_def rational_approximation)
-  then show ?thesis by auto
-qed
-
-proposition matrix_rational_approximation:
-  fixes A :: "real^'n^'m"
-  assumes "e > 0"
-  obtains B where "\<And>i j. B$i$j \<in> \<rat>" "onorm(\<lambda>x. (A - B) *v x) < e"
-proof -
-  have "\<forall>i j. \<exists>q \<in> \<rat>. \<bar>q - A $ i $ j\<bar> < e / (2 * CARD('m) * CARD('n))"
-    using assms by (force intro: rational_approximation [of "e / (2 * CARD('m) * CARD('n))"])
-  then obtain B where B: "\<And>i j. B$i$j \<in> \<rat>" and Bclo: "\<And>i j. \<bar>B$i$j - A $ i $ j\<bar> < e / (2 * CARD('m) * CARD('n))"
-    by (auto simp: lambda_skolem Bex_def)
-  show ?thesis
-  proof
-    have "onorm ((*v) (A - B)) \<le> real CARD('m) * real CARD('n) *
-    (e / (2 * real CARD('m) * real CARD('n)))"
-      apply (rule onorm_le_matrix_component)
-      using Bclo by (simp add: abs_minus_commute less_imp_le)
-    also have "\<dots> < e"
-      using \<open>0 < e\<close> by (simp add: field_split_simps)
-    finally show "onorm ((*v) (A - B)) < e" .
-  qed (use B in auto)
-qed
-
 lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
   unfolding inner_simps scalar_mult_eq_scaleR by auto
 
@@ -478,6 +445,42 @@
 qed
 *)
 
+subsection\<open>Arbitrarily good rational approximations\<close>
+
+lemma rational_approximation:
+  assumes "e > 0"
+  obtains r::real where "r \<in> \<rat>" "\<bar>r - x\<bar> < e"
+  using Rats_dense_in_real [of "x - e/2" "x + e/2"] assms by auto
+
+lemma Rats_closure_real: "closure \<rat> = (UNIV::real set)"
+proof -
+  have "\<And>x::real. x \<in> closure \<rat>"
+    by (metis closure_approachable dist_real_def rational_approximation)
+  then show ?thesis by auto
+qed
+
+proposition matrix_rational_approximation:
+  fixes A :: "real^'n^'m"
+  assumes "e > 0"
+  obtains B where "\<And>i j. B$i$j \<in> \<rat>" "onorm(\<lambda>x. (A - B) *v x) < e"
+proof -
+  have "\<forall>i j. \<exists>q \<in> \<rat>. \<bar>q - A $ i $ j\<bar> < e / (2 * CARD('m) * CARD('n))"
+    using assms by (force intro: rational_approximation [of "e / (2 * CARD('m) * CARD('n))"])
+  then obtain B where B: "\<And>i j. B$i$j \<in> \<rat>" and Bclo: "\<And>i j. \<bar>B$i$j - A $ i $ j\<bar> < e / (2 * CARD('m) * CARD('n))"
+    by (auto simp: lambda_skolem Bex_def)
+  show ?thesis
+  proof
+    have "onorm ((*v) (A - B)) \<le> real CARD('m) * real CARD('n) *
+    (e / (2 * real CARD('m) * real CARD('n)))"
+      apply (rule onorm_le_matrix_component)
+      using Bclo by (simp add: abs_minus_commute less_imp_le)
+    also have "\<dots> < e"
+      using \<open>0 < e\<close> by (simp add: field_split_simps)
+    finally show "onorm ((*v) (A - B)) < e" .
+  qed (use B in auto)
+qed
+
+
 subsection "Derivative"
 
 definition\<^marker>\<open>tag important\<close> "jacobian f net = matrix(frechet_derivative f net)"
@@ -547,8 +550,7 @@
 lemma interval_split_cart:
   "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
   "cbox a b \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
-  apply (rule_tac[!] set_eqI)
-  unfolding Int_iff mem_box_cart mem_Collect_eq interval_cbox_cart
+  unfolding Int_iff mem_box_cart mem_Collect_eq interval_cbox_cart set_eq_iff
   unfolding vec_lambda_beta
   by auto
 
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Sun May 07 14:52:53 2023 +0100
@@ -1323,32 +1323,6 @@
 lemma at_within_eq_bot_iff: "at c within A = bot \<longleftrightarrow> c \<notin> closure (A - {c})"
   using not_trivial_limit_within[of c A] by blast
 
-text \<open>Some property holds "sufficiently close" to the limit point.\<close>
-
-lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
-  by simp
-
-lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
-  by (simp add: filter_eq_iff)
-
-lemma Lim_topological:
-  "(f \<longlongrightarrow> l) net \<longleftrightarrow>
-    trivial_limit net \<or> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
-  unfolding tendsto_def trivial_limit_eq by auto
-
-lemma eventually_within_Un:
-  "eventually P (at x within (s \<union> t)) \<longleftrightarrow>
-    eventually P (at x within s) \<and> eventually P (at x within t)"
-  unfolding eventually_at_filter
-  by (auto elim!: eventually_rev_mp)
-
-lemma Lim_within_union:
- "(f \<longlongrightarrow> l) (at x within (s \<union> t)) \<longleftrightarrow>
-  (f \<longlongrightarrow> l) (at x within s) \<and> (f \<longlongrightarrow> l) (at x within t)"
-  unfolding tendsto_def
-  by (auto simp: eventually_within_Un)
-
-
 subsection \<open>Limits\<close>
 
 text \<open>The expected monotonicity property.\<close>
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Sun May 07 14:52:53 2023 +0100
@@ -2313,6 +2313,174 @@
   using assms homeomorphic_map_path_component_of by fastforce
 
 
+subsection\<open>Paths and path-connectedness\<close>
+
+lemma path_connected_space_quotient_map_image:
+   "\<lbrakk>quotient_map X Y q; path_connected_space X\<rbrakk> \<Longrightarrow> path_connected_space Y"
+  by (metis path_connectedin_continuous_map_image path_connectedin_topspace quotient_imp_continuous_map quotient_imp_surjective_map)
+
+lemma path_connected_space_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; path_connected_space X\<rbrakk> \<Longrightarrow> path_connected_space Y"
+  using path_connected_space_quotient_map_image retraction_imp_quotient_map by blast
+
+lemma path_connected_space_prod_topology:
+  "path_connected_space(prod_topology X Y) \<longleftrightarrow>
+        topspace(prod_topology X Y) = {} \<or> path_connected_space X \<and> path_connected_space Y"
+proof (cases "topspace(prod_topology X Y) = {}")
+  case True
+  then show ?thesis
+    by (simp add: path_connected_space_topspace_empty)
+next
+  case False
+  have "path_connected_space (prod_topology X Y)" 
+    if X: "path_connected_space X" and Y: "path_connected_space Y"
+  proof (clarsimp simp: path_connected_space_def)
+    fix x y x' y'
+    assume "x \<in> topspace X" and "y \<in> topspace Y" and "x' \<in> topspace X" and "y' \<in> topspace Y"
+    obtain f where "pathin X f" "f 0 = x" "f 1 = x'"
+      by (meson X \<open>x \<in> topspace X\<close> \<open>x' \<in> topspace X\<close> path_connected_space_def)
+    obtain g where "pathin Y g" "g 0 = y" "g 1 = y'"
+      by (meson Y \<open>y \<in> topspace Y\<close> \<open>y' \<in> topspace Y\<close> path_connected_space_def)
+    show "\<exists>h. pathin (prod_topology X Y) h \<and> h 0 = (x,y) \<and> h 1 = (x',y')"
+    proof (intro exI conjI)
+      show "pathin (prod_topology X Y) (\<lambda>t. (f t, g t))"
+        using \<open>pathin X f\<close> \<open>pathin Y g\<close> by (simp add: continuous_map_paired pathin_def)
+      show "(\<lambda>t. (f t, g t)) 0 = (x, y)"
+        using \<open>f 0 = x\<close> \<open>g 0 = y\<close> by blast
+      show "(\<lambda>t. (f t, g t)) 1 = (x', y')"
+        using \<open>f 1 = x'\<close> \<open>g 1 = y'\<close> by blast
+    qed
+  qed
+  then show ?thesis
+    by (metis False Sigma_empty1 Sigma_empty2 topspace_prod_topology path_connected_space_retraction_map_image
+        retraction_map_fst  retraction_map_snd) 
+qed
+
+lemma path_connectedin_Times:
+   "path_connectedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow>
+        S = {} \<or> T = {} \<or> path_connectedin X S \<and> path_connectedin Y T"
+  by (auto simp add: path_connectedin_def subtopology_Times path_connected_space_prod_topology)
+
+
+subsection\<open>Path components\<close>
+
+lemma path_component_of_subtopology_eq:
+  "path_component_of (subtopology X U) x = path_component_of X x \<longleftrightarrow> path_component_of_set X x \<subseteq> U"  
+  (is "?lhs = ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (metis path_connectedin_path_component_of path_connectedin_subtopology)
+next
+  show "?rhs \<Longrightarrow> ?lhs"
+    unfolding fun_eq_iff
+    by (metis path_connectedin_subtopology path_component_of path_component_of_aux path_component_of_mono)
+qed
+
+lemma path_components_of_subtopology:
+  assumes "C \<in> path_components_of X" "C \<subseteq> U"
+  shows "C \<in> path_components_of (subtopology X U)"
+  using assms path_component_of_refl path_component_of_subtopology_eq topspace_subtopology
+  by (smt (verit) imageE path_component_in_path_components_of path_components_of_def)
+
+lemma path_imp_connected_component_of:
+   "path_component_of X x y \<Longrightarrow> connected_component_of X x y"
+  by (metis in_mono mem_Collect_eq path_component_subset_connected_component_of)
+
+lemma finite_path_components_of_finite:
+   "finite(topspace X) \<Longrightarrow> finite(path_components_of X)"
+  by (simp add: Union_path_components_of finite_UnionD)
+
+lemma path_component_of_continuous_image:
+  "\<lbrakk>continuous_map X X' f; path_component_of X x y\<rbrakk> \<Longrightarrow> path_component_of X' (f x) (f y)"
+  by (meson image_eqI path_component_of path_connectedin_continuous_map_image)
+
+lemma path_component_of_pair [simp]:
+   "path_component_of_set (prod_topology X Y) (x,y) =
+    path_component_of_set X x \<times> path_component_of_set Y y"   (is "?lhs = ?rhs")
+proof (cases "?lhs = {}")
+  case True
+  then show ?thesis
+    by (metis Sigma_empty1 Sigma_empty2 mem_Sigma_iff path_component_of_eq_empty topspace_prod_topology) 
+next
+  case False
+  then have "path_component_of X x x" "path_component_of Y y y"
+    using path_component_of_eq_empty path_component_of_refl by fastforce+
+  moreover
+  have "path_connectedin (prod_topology X Y) (path_component_of_set X x \<times> path_component_of_set Y y)"
+    by (metis path_connectedin_Times path_connectedin_path_component_of)
+  moreover have "path_component_of X x a" "path_component_of Y y b"
+    if "(x, y) \<in> C'" "(a,b) \<in> C'" and "path_connectedin (prod_topology X Y) C'" for C' a b
+    by (smt (verit, best) that continuous_map_fst continuous_map_snd fst_conv snd_conv path_component_of path_component_of_continuous_image)+
+  ultimately show ?thesis
+    by (intro path_component_of_unique) auto
+qed
+
+lemma path_components_of_prod_topology:
+   "path_components_of (prod_topology X Y) =
+    (\<lambda>(C,D). C \<times> D) ` (path_components_of X \<times> path_components_of Y)"
+  by (force simp add: image_iff path_components_of_def)
+
+lemma path_components_of_prod_topology':
+   "path_components_of (prod_topology X Y) =
+    {C \<times> D |C D. C \<in> path_components_of X \<and> D \<in> path_components_of Y}"
+  by (auto simp: path_components_of_prod_topology)
+
+lemma path_component_of_product_topology:
+   "path_component_of_set (product_topology X I) f =
+    (if f \<in> extensional I then PiE I (\<lambda>i. path_component_of_set (X i) (f i)) else {})"
+    (is "?lhs = ?rhs")
+proof (cases "path_component_of_set (product_topology X I) f = {}")
+  case True
+  then show ?thesis
+    by (smt (verit) PiE_eq_empty_iff PiE_iff path_component_of_eq_empty topspace_product_topology)
+next
+  case False
+  then have [simp]: "f \<in> extensional I"
+    by (auto simp: path_component_of_eq_empty PiE_iff path_component_of_equiv)
+  show ?thesis
+  proof (intro path_component_of_unique)
+    show "f \<in> ?rhs"
+      using False path_component_of_eq_empty path_component_of_refl by force
+    show "path_connectedin (product_topology X I) (if f \<in> extensional I then \<Pi>\<^sub>E i\<in>I. path_component_of_set (X i) (f i) else {})"
+      by (simp add: path_connectedin_PiE path_connectedin_path_component_of)
+    fix C'
+    assume "f \<in> C'" and C': "path_connectedin (product_topology X I) C'" 
+    show "C' \<subseteq> ?rhs"
+    proof -
+      have "C' \<subseteq> extensional I"
+        using PiE_def C' path_connectedin_subset_topspace by fastforce
+      with \<open>f \<in> C'\<close> C' show ?thesis
+        apply (clarsimp simp: PiE_iff subset_iff)
+        by (smt (verit, ccfv_threshold) continuous_map_product_projection path_component_of path_component_of_continuous_image)
+    qed   
+  qed
+qed
+
+lemma path_components_of_product_topology:
+  "path_components_of (product_topology X I) =
+    {PiE I B |B. \<forall>i \<in> I. B i \<in> path_components_of(X i)}"  (is "?lhs=?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    apply (simp add: path_components_of_def image_subset_iff)
+    by (smt (verit, best) PiE_iff image_eqI path_component_of_product_topology)
+next
+  show "?rhs \<subseteq> ?lhs"
+  proof
+    fix F
+    assume "F \<in> ?rhs"
+    then obtain B where B: "F = Pi\<^sub>E I B"
+      and "\<forall>i\<in>I. \<exists>x\<in>topspace (X i). B i = path_component_of_set (X i) x"
+      by (force simp add: path_components_of_def image_iff)
+    then obtain f where ftop: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> topspace (X i)"
+      and BF: "\<And>i. i \<in> I \<Longrightarrow> B i = path_component_of_set (X i) (f i)"
+      by metis
+    then have "F = path_component_of_set (product_topology X I) (restrict f I)"
+      by (metis (mono_tags, lifting) B PiE_cong path_component_of_product_topology restrict_apply' restrict_extensional)
+    then show "F \<in> ?lhs"
+      by (simp add: ftop path_component_in_path_components_of)
+  qed
+qed
+
 subsection \<open>Sphere is path-connected\<close>
 
 lemma path_connected_punctured_universe:
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy	Sun May 07 14:52:53 2023 +0100
@@ -49,6 +49,9 @@
   apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_singleton)
   using t1_space_alt by auto
 
+lemma t1_space_euclidean: "t1_space (euclidean :: 'a::metric_space topology)"
+  by (simp add: t1_space_closedin_singleton)
+
 lemma closedin_t1_singleton:
    "\<lbrakk>t1_space X; a \<in> topspace X\<rbrakk> \<Longrightarrow> closedin X {a}"
   by (simp add: t1_space_closedin_singleton)
@@ -743,5 +746,5 @@
     qed
   qed
 qed fastforce
-    
+
 end
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Filter.thy	Sun May 07 14:52:53 2023 +0100
@@ -458,6 +458,12 @@
 lemma False_imp_not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> \<not> trivial_limit net \<Longrightarrow> \<not> eventually (\<lambda>x. P x) net"
   by (simp add: eventually_False)
 
+lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
+  by simp
+
+lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
+  by (simp add: filter_eq_iff)
+
 lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
 proof -
   let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Limits.thy	Sun May 07 14:52:53 2023 +0100
@@ -3251,4 +3251,21 @@
   for f :: "real \<Rightarrow> real"
   using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp: neq_iff)
 
+lemma Lim_topological:
+  "(f \<longlongrightarrow> l) net \<longleftrightarrow>
+    trivial_limit net \<or> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
+  unfolding tendsto_def trivial_limit_eq by auto
+
+lemma eventually_within_Un:
+  "eventually P (at x within (s \<union> t)) \<longleftrightarrow>
+    eventually P (at x within s) \<and> eventually P (at x within t)"
+  unfolding eventually_at_filter
+  by (auto elim!: eventually_rev_mp)
+
+lemma Lim_within_Un:
+ "(f \<longlongrightarrow> l) (at x within (s \<union> t)) \<longleftrightarrow>
+  (f \<longlongrightarrow> l) (at x within s) \<and> (f \<longlongrightarrow> l) (at x within t)"
+  unfolding tendsto_def
+  by (auto simp: eventually_within_Un)
+
 end
diff -r 30f69046f120 -r ffdad62bc235 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Sat May 06 12:42:10 2023 +0100
+++ b/src/HOL/Real.thy	Sun May 07 14:52:53 2023 +0100
@@ -1402,10 +1402,34 @@
 lemma forall_pos_mono_1:
   "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
     (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
-  apply (rule forall_pos_mono)
-  apply auto
-  apply (metis Suc_pred of_nat_Suc)
-  done
+  using reals_Archimedean by blast
+
+lemma Archimedean_eventually_pow:
+  fixes x::real
+  assumes "1 < x"
+  shows "\<forall>\<^sub>F n in sequentially. b < x ^ n"
+proof -
+  obtain N where "\<And>n. n\<ge>N \<Longrightarrow> b < x ^ n"
+    by (metis assms le_less order_less_trans power_strict_increasing_iff real_arch_pow)
+  then show ?thesis
+    using eventually_sequentially by blast
+qed
+
+lemma Archimedean_eventually_pow_inverse:
+  fixes x::real
+  assumes "\<bar>x\<bar> < 1" "\<epsilon> > 0"
+  shows "\<forall>\<^sub>F n in sequentially. \<bar>x^n\<bar> < \<epsilon>"
+proof (cases "x = 0")
+  case True
+  then show ?thesis
+    by (simp add: assms eventually_at_top_dense zero_power)
+next
+  case False
+  then have "\<forall>\<^sub>F n in sequentially. inverse \<epsilon> < inverse \<bar>x\<bar> ^ n"
+    by (simp add: Archimedean_eventually_pow assms(1) one_less_inverse)
+  then show ?thesis
+    by eventually_elim (metis \<open>\<epsilon> > 0\<close> inverse_less_imp_less power_abs power_inverse)
+qed
 
 
 subsection \<open>Floor and Ceiling Functions from the Reals to the Integers\<close>