src/HOL/Analysis/Continuous_Extension.thy

   case False
     have nonneg: "0 \<le> supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" for x
       by (simp add: supp_sum_def sum_nonneg)
     have sd_pos: "0 < setdist {x} (S - V)" if "V \<in> \<C>" "x \<in> S" "x \<in> V" for V x
     proof -
-      have "closedin (subtopology euclidean S) (S - V)"
+      have "closedin (top_of_set S) (S - V)"
         by (simp add: Diff_Diff_Int closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
       with that False  setdist_pos_le [of "{x}" "S - V"]
       show ?thesis
         using setdist_gt_0_closedin by fastforce
     qed

         have *: "continuous_on S (\<lambda>x. supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>)"
         proof (clarsimp simp add: continuous_on_eq_continuous_within)
           fix x assume "x \<in> S"
           then obtain X where "open X" and x: "x \<in> S \<inter> X" and finX: "finite {U \<in> \<C>. U \<inter> X \<noteq> {}}"
             using assms by blast
-          then have OSX: "openin (subtopology euclidean S) (S \<inter> X)" by blast
+          then have OSX: "openin (top_of_set S) (S \<inter> X)" by blast
           have sumeq: "\<And>x. x \<in> S \<inter> X \<Longrightarrow>
                      (\<Sum>V | V \<in> \<C> \<and> V \<inter> X \<noteq> {}. setdist {x} (S - V))
                      = supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>"
             apply (simp add: supp_sum_def)
             apply (rule sum.mono_neutral_right [OF finX])

 subsection\<open>Urysohn's Lemma for Euclidean Spaces\<close>
 
 text \<open>For Euclidean spaces the proof is easy using distances.\<close>
 
 lemma Urysohn_both_ne:
-  assumes US: "closedin (subtopology euclidean U) S"
-      and UT: "closedin (subtopology euclidean U) T"
+  assumes US: "closedin (top_of_set U) S"
+      and UT: "closedin (top_of_set U) T"
       and "S \<inter> T = {}" "S \<noteq> {}" "T \<noteq> {}" "a \<noteq> b"
   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
     where "continuous_on U f"
           "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
           "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"

     qed
   qed
 qed
 
 proposition Urysohn_local_strong:
-  assumes US: "closedin (subtopology euclidean U) S"
-      and UT: "closedin (subtopology euclidean U) T"
+  assumes US: "closedin (top_of_set U) S"
+      and UT: "closedin (top_of_set U) T"
       and "S \<inter> T = {}" "a \<noteq> b"
   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
     where "continuous_on U f"
           "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
           "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"

       by blast
   qed
 qed
 
 lemma Urysohn_local:
-  assumes US: "closedin (subtopology euclidean U) S"
-      and UT: "closedin (subtopology euclidean U) T"
+  assumes US: "closedin (top_of_set U) S"
+      and UT: "closedin (top_of_set U) T"
       and "S \<inter> T = {}"
   obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
     where "continuous_on U f"
           "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
           "\<And>x. x \<in> S \<Longrightarrow> f x = a"

 text \<open>See \cite{dugundji}.\<close>
 
 theorem Dugundji:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   assumes "convex C" "C \<noteq> {}"
-      and cloin: "closedin (subtopology euclidean U) S"
+      and cloin: "closedin (top_of_set U) S"
       and contf: "continuous_on S f" and "f ` S \<subseteq> C"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C"
                   "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
 proof (cases "S = {}")
   case True then show thesis

       next
         case False
         obtain N where N: "open N" "a \<in> N"
                    and finN: "finite {U \<in> \<C>. \<exists>a\<in>N. H U a \<noteq> 0}"
           using Hfin False \<open>a \<in> U\<close> by auto
-        have oUS: "openin (subtopology euclidean U) (U - S)"
+        have oUS: "openin (top_of_set U) (U - S)"
           using cloin by (simp add: openin_diff)
         have HcontU: "continuous (at a within U) (H T)" if "T \<in> \<C>" for T
           using Hcont [OF \<open>T \<in> \<C>\<close>] False  \<open>a \<in> U\<close> \<open>T \<in> \<C>\<close>
           apply (simp add: continuous_on_eq_continuous_within continuous_within)
           apply (rule Lim_transform_within_set)

           proof (rule continuous_transform_within_openin)
             show "continuous (at a within U)
                     (\<lambda>x. \<Sum>T\<in>{U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))"
               by (force intro: continuous_intros HcontU)+
           next
-            show "openin (subtopology euclidean U) ((U - S) \<inter> N)"
+            show "openin (top_of_set U) ((U - S) \<inter> N)"
               using N oUS openin_trans by blast
           next
             show "a \<in> (U - S) \<inter> N" using False \<open>a \<in> U\<close> N by blast
           next
             show "\<And>x. x \<in> (U - S) \<inter> N \<Longrightarrow>

 
 
 corollary Tietze:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   assumes "continuous_on S f"
-    and "closedin (subtopology euclidean U) S"
+    and "closedin (top_of_set U) S"
     and "0 \<le> B"
     and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
   using assms by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
 
 corollary%unimportant Tietze_closed_interval:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f"
-    and "closedin (subtopology euclidean U) S"
+    and "closedin (top_of_set U) S"
     and "cbox a b \<noteq> {}"
     and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
   apply (rule Dugundji [of "cbox a b" U S f])
   using assms by auto
 
 corollary%unimportant Tietze_closed_interval_1:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
   assumes "continuous_on S f"
-    and "closedin (subtopology euclidean U) S"
+    and "closedin (top_of_set U) S"
     and "a \<le> b"
     and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
   apply (rule Dugundji [of "cbox a b" U S f])
   using assms by (auto simp: image_subset_iff)
 
 corollary%unimportant Tietze_open_interval:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f"
-    and "closedin (subtopology euclidean U) S"
+    and "closedin (top_of_set U) S"
     and "box a b \<noteq> {}"
     and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
   apply (rule Dugundji [of "box a b" U S f])
   using assms by auto
 
 corollary%unimportant Tietze_open_interval_1:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
   assumes "continuous_on S f"
-    and "closedin (subtopology euclidean U) S"
+    and "closedin (top_of_set U) S"
     and "a < b"
     and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
   apply (rule Dugundji [of "box a b" U S f])
   using assms by (auto simp: image_subset_iff)
 
 corollary%unimportant Tietze_unbounded:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   assumes "continuous_on S f"
-    and "closedin (subtopology euclidean U) S"
+    and "closedin (top_of_set U) S"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   apply (rule Dugundji [of UNIV U S f])
   using assms by auto
 
 end