# HG changeset patch
# User nipkow
# Date 1755070497 -7200
# Node ID 304519f22c2ce13b646ae8e2864ae808482f1f35
# Parent  7ac70210d12cc5d99ad035c52ed0c470764cca92# Parent  1ee42e4832aa37de30abd26474f79292bd4f3919
prefer existing proof in Abstract_Topological_Spaces

diff -r 1ee42e4832aa -r 304519f22c2c src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Wed Aug 13 09:20:25 2025 +0200
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Wed Aug 13 09:34:57 2025 +0200
@@ -3266,6 +3266,11 @@
                      "\<not> disjnt V {x. x \<in> topspace X \<and> f x = b}" 
      for a b U V
     proof -
+      have closedin_topspace: "closedin X {x \<in> topspace X. f x \<in> {y..z}}" for y z
+        using closed_real_atLeastAtMost[unfolded closed_closedin]
+          \<open>continuous_map X euclideanreal f\<close>[unfolded continuous_map_closedin]
+        by blast
+
       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
@@ -3279,8 +3284,8 @@
         case 1
         define W where "W \<equiv> {x \<in> topspace X. f x \<in> {a..b}}"
         have "closedin X W"
-           using closed_real_atLeastAtMost assms
-           unfolding W_def closed_closedin continuous_map_closedin by blast 
+          unfolding W_def
+          using closedin_topspace .
         show ?thesis
         proof (rule * [OF 1 , of "U \<inter> W" "V \<inter> W"])
           show "closedin X (U \<inter> W)" "closedin X (V \<inter> W)"
@@ -3306,8 +3311,8 @@
         case 3
         define W where "W \<equiv> {x \<in> topspace X. f x \<in> {b..a}}"
         have "closedin X W"
-           using closed_real_atLeastAtMost assms
-           unfolding W_def closed_closedin continuous_map_closedin by blast 
+          unfolding W_def
+          using closedin_topspace .
         show ?thesis
         proof (rule * [OF 3, of "V \<inter> W" "U \<inter> W"])
           show "closedin X (U \<inter> W)" "closedin X (V \<inter> W)"