src/HOL/Analysis/Homotopy.thy
changeset 69922 4a9167f377b0
parent 69918 eddcc7c726f3
child 69986 f2d327275065
     1.1 --- a/src/HOL/Analysis/Homotopy.thy	Mon Mar 18 15:35:34 2019 +0000
     1.2 +++ b/src/HOL/Analysis/Homotopy.thy	Tue Mar 19 16:14:51 2019 +0000
     1.3 @@ -258,12 +258,12 @@
     1.4      assumes "homotopic_with P X Y f g" and "homotopic_with P X Y g h"
     1.5        shows "homotopic_with P X Y f h"
     1.6  proof -
     1.7 -  have clo1: "closedin (subtopology euclidean ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({0..1/2::real} \<times> X)"
     1.8 +  have clo1: "closedin (top_of_set ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({0..1/2::real} \<times> X)"
     1.9      apply (simp add: closedin_closed split_01_prod [symmetric])
    1.10      apply (rule_tac x="{0..1/2} \<times> UNIV" in exI)
    1.11      apply (force simp: closed_Times)
    1.12      done
    1.13 -  have clo2: "closedin (subtopology euclidean ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({1/2..1::real} \<times> X)"
    1.14 +  have clo2: "closedin (top_of_set ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({1/2..1::real} \<times> X)"
    1.15      apply (simp add: closedin_closed split_01_prod [symmetric])
    1.16      apply (rule_tac x="{1/2..1} \<times> UNIV" in exI)
    1.17      apply (force simp: closed_Times)
    1.18 @@ -1472,20 +1472,20 @@
    1.19  definition%important locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
    1.20  where
    1.21   "locally P S \<equiv>
    1.22 -        \<forall>w x. openin (subtopology euclidean S) w \<and> x \<in> w
    1.23 -              \<longrightarrow> (\<exists>u v. openin (subtopology euclidean S) u \<and> P v \<and>
    1.24 +        \<forall>w x. openin (top_of_set S) w \<and> x \<in> w
    1.25 +              \<longrightarrow> (\<exists>u v. openin (top_of_set S) u \<and> P v \<and>
    1.26                          x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)"
    1.27  
    1.28  lemma locallyI:
    1.29 -  assumes "\<And>w x. \<lbrakk>openin (subtopology euclidean S) w; x \<in> w\<rbrakk>
    1.30 -                  \<Longrightarrow> \<exists>u v. openin (subtopology euclidean S) u \<and> P v \<and>
    1.31 +  assumes "\<And>w x. \<lbrakk>openin (top_of_set S) w; x \<in> w\<rbrakk>
    1.32 +                  \<Longrightarrow> \<exists>u v. openin (top_of_set S) u \<and> P v \<and>
    1.33                          x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w"
    1.34      shows "locally P S"
    1.35  using assms by (force simp: locally_def)
    1.36  
    1.37  lemma locallyE:
    1.38 -  assumes "locally P S" "openin (subtopology euclidean S) w" "x \<in> w"
    1.39 -  obtains u v where "openin (subtopology euclidean S) u"
    1.40 +  assumes "locally P S" "openin (top_of_set S) w" "x \<in> w"
    1.41 +  obtains u v where "openin (top_of_set S) u"
    1.42                      "P v" "x \<in> u" "u \<subseteq> v" "v \<subseteq> w"
    1.43    using assms unfolding locally_def by meson
    1.44  
    1.45 @@ -1495,7 +1495,7 @@
    1.46  by (metis assms locally_def)
    1.47  
    1.48  lemma locally_open_subset:
    1.49 -  assumes "locally P S" "openin (subtopology euclidean S) t"
    1.50 +  assumes "locally P S" "openin (top_of_set S) t"
    1.51      shows "locally P t"
    1.52  using assms
    1.53  apply (simp add: locally_def)
    1.54 @@ -1507,7 +1507,7 @@
    1.55  by (metis (no_types, hide_lams) Int_absorb1 Int_lower1 Int_subset_iff openin_open openin_subtopology_Int_subset)
    1.56  
    1.57  lemma locally_diff_closed:
    1.58 -    "\<lbrakk>locally P S; closedin (subtopology euclidean S) t\<rbrakk> \<Longrightarrow> locally P (S - t)"
    1.59 +    "\<lbrakk>locally P S; closedin (top_of_set S) t\<rbrakk> \<Longrightarrow> locally P (S - t)"
    1.60    using locally_open_subset closedin_def by fastforce
    1.61  
    1.62  lemma locally_empty [iff]: "locally P {}"
    1.63 @@ -1550,15 +1550,15 @@
    1.64      unfolding locally_def
    1.65  proof (clarify)
    1.66    fix W x y
    1.67 -  assume W: "openin (subtopology euclidean (S \<times> T)) W" and xy: "(x, y) \<in> W"
    1.68 -  then obtain U V where "openin (subtopology euclidean S) U" "x \<in> U"
    1.69 -                        "openin (subtopology euclidean T) V" "y \<in> V" "U \<times> V \<subseteq> W"
    1.70 +  assume W: "openin (top_of_set (S \<times> T)) W" and xy: "(x, y) \<in> W"
    1.71 +  then obtain U V where "openin (top_of_set S) U" "x \<in> U"
    1.72 +                        "openin (top_of_set T) V" "y \<in> V" "U \<times> V \<subseteq> W"
    1.73      using Times_in_interior_subtopology by metis
    1.74    then obtain U1 U2 V1 V2
    1.75 -         where opeS: "openin (subtopology euclidean S) U1 \<and> P U2 \<and> x \<in> U1 \<and> U1 \<subseteq> U2 \<and> U2 \<subseteq> U"
    1.76 -           and opeT: "openin (subtopology euclidean T) V1 \<and> Q V2 \<and> y \<in> V1 \<and> V1 \<subseteq> V2 \<and> V2 \<subseteq> V"
    1.77 +         where opeS: "openin (top_of_set S) U1 \<and> P U2 \<and> x \<in> U1 \<and> U1 \<subseteq> U2 \<and> U2 \<subseteq> U"
    1.78 +           and opeT: "openin (top_of_set T) V1 \<and> Q V2 \<and> y \<in> V1 \<and> V1 \<subseteq> V2 \<and> V2 \<subseteq> V"
    1.79      by (meson PS QT locallyE)
    1.80 -  with \<open>U \<times> V \<subseteq> W\<close> show "\<exists>u v. openin (subtopology euclidean (S \<times> T)) u \<and> R v \<and> (x,y) \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> W"
    1.81 +  with \<open>U \<times> V \<subseteq> W\<close> show "\<exists>u v. openin (top_of_set (S \<times> T)) u \<and> R v \<and> (x,y) \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> W"
    1.82      apply (rule_tac x="U1 \<times> V1" in exI)
    1.83      apply (rule_tac x="U2 \<times> V2" in exI)
    1.84      apply (auto simp: openin_Times R)
    1.85 @@ -1573,7 +1573,7 @@
    1.86      shows "locally Q t"
    1.87  proof (clarsimp simp: locally_def)
    1.88    fix W y
    1.89 -  assume "y \<in> W" and "openin (subtopology euclidean t) W"
    1.90 +  assume "y \<in> W" and "openin (top_of_set t) W"
    1.91    then obtain T where T: "open T" "W = t \<inter> T"
    1.92      by (force simp: openin_open)
    1.93    then have "W \<subseteq> t" by auto
    1.94 @@ -1586,15 +1586,15 @@
    1.95      using \<open>g ` t = S\<close> \<open>W \<subseteq> t\<close> apply blast
    1.96      using g \<open>W \<subseteq> t\<close> apply auto[1]
    1.97      by (simp add: f rev_image_eqI)
    1.98 -  have \<circ>: "openin (subtopology euclidean S) (g ` W)"
    1.99 +  have \<circ>: "openin (top_of_set S) (g ` W)"
   1.100    proof -
   1.101      have "continuous_on S f"
   1.102        using f(3) by blast
   1.103 -    then show "openin (subtopology euclidean S) (g ` W)"
   1.104 -      by (simp add: gw Collect_conj_eq \<open>openin (subtopology euclidean t) W\<close> continuous_on_open f(2))
   1.105 +    then show "openin (top_of_set S) (g ` W)"
   1.106 +      by (simp add: gw Collect_conj_eq \<open>openin (top_of_set t) W\<close> continuous_on_open f(2))
   1.107    qed
   1.108    then obtain u v
   1.109 -    where osu: "openin (subtopology euclidean S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` W"
   1.110 +    where osu: "openin (top_of_set S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` W"
   1.111      using S [unfolded locally_def, rule_format, of "g ` W" "g y"] \<open>y \<in> W\<close> by force
   1.112    have "v \<subseteq> S" using uv by (simp add: gw)
   1.113    have fv: "f ` v = t \<inter> {x. g x \<in> v}"
   1.114 @@ -1609,7 +1609,7 @@
   1.115      using \<open>v \<subseteq> S\<close> \<open>W \<subseteq> t\<close> f
   1.116      apply (simp add: homeomorphism_def contvf contvg, auto)
   1.117      by (metis f(1) rev_image_eqI rev_subsetD)
   1.118 -  have 1: "openin (subtopology euclidean t) (t \<inter> g -` u)"
   1.119 +  have 1: "openin (top_of_set t) (t \<inter> g -` u)"
   1.120      apply (rule continuous_on_open [THEN iffD1, rule_format])
   1.121      apply (rule \<open>continuous_on t g\<close>)
   1.122      using \<open>g ` t = S\<close> apply (simp add: osu)
   1.123 @@ -1619,7 +1619,7 @@
   1.124      apply (intro conjI Q [OF \<open>P v\<close> homv])
   1.125      using \<open>W \<subseteq> t\<close> \<open>y \<in> W\<close>  \<open>f ` v \<subseteq> W\<close>  uv  apply (auto simp: fv)
   1.126      done
   1.127 -  show "\<exists>U. openin (subtopology euclidean t) U \<and> (\<exists>v. Q v \<and> y \<in> U \<and> U \<subseteq> v \<and> v \<subseteq> W)"
   1.128 +  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)"
   1.129      by (meson 1 2)
   1.130  qed
   1.131  
   1.132 @@ -1674,23 +1674,23 @@
   1.133    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   1.134    assumes P: "locally P S"
   1.135        and f: "continuous_on S f"
   1.136 -      and oo: "\<And>t. openin (subtopology euclidean S) t
   1.137 -                   \<Longrightarrow> openin (subtopology euclidean (f ` S)) (f ` t)"
   1.138 +      and oo: "\<And>t. openin (top_of_set S) t
   1.139 +                   \<Longrightarrow> openin (top_of_set (f ` S)) (f ` t)"
   1.140        and Q: "\<And>t. \<lbrakk>t \<subseteq> S; P t\<rbrakk> \<Longrightarrow> Q(f ` t)"
   1.141      shows "locally Q (f ` S)"
   1.142  proof (clarsimp simp add: locally_def)
   1.143    fix W y
   1.144 -  assume oiw: "openin (subtopology euclidean (f ` S)) W" and "y \<in> W"
   1.145 +  assume oiw: "openin (top_of_set (f ` S)) W" and "y \<in> W"
   1.146    then have "W \<subseteq> f ` S" by (simp add: openin_euclidean_subtopology_iff)
   1.147 -  have oivf: "openin (subtopology euclidean S) (S \<inter> f -` W)"
   1.148 +  have oivf: "openin (top_of_set S) (S \<inter> f -` W)"
   1.149      by (rule continuous_on_open [THEN iffD1, rule_format, OF f oiw])
   1.150    then obtain x where "x \<in> S" "f x = y"
   1.151      using \<open>W \<subseteq> f ` S\<close> \<open>y \<in> W\<close> by blast
   1.152    then obtain U V
   1.153 -    where "openin (subtopology euclidean S) U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> S \<inter> f -` W"
   1.154 +    where "openin (top_of_set S) U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> S \<inter> f -` W"
   1.155      using P [unfolded locally_def, rule_format, of "(S \<inter> f -` W)" x] oivf \<open>y \<in> W\<close>
   1.156      by auto
   1.157 -  then show "\<exists>X. openin (subtopology euclidean (f ` S)) X \<and> (\<exists>Y. Q Y \<and> y \<in> X \<and> X \<subseteq> Y \<and> Y \<subseteq> W)"
   1.158 +  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)"
   1.159      apply (rule_tac x="f ` U" in exI)
   1.160      apply (rule conjI, blast intro!: oo)
   1.161      apply (rule_tac x="f ` V" in exI)
   1.162 @@ -1703,21 +1703,21 @@
   1.163  
   1.164  proposition connected_induction:
   1.165    assumes "connected S"
   1.166 -      and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
   1.167 +      and opD: "\<And>T a. \<lbrakk>openin (top_of_set S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
   1.168        and opI: "\<And>a. a \<in> S
   1.169 -             \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and>
   1.170 +             \<Longrightarrow> \<exists>T. openin (top_of_set S) T \<and> a \<in> T \<and>
   1.171                       (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<and> Q x \<longrightarrow> Q y)"
   1.172        and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
   1.173      shows "Q b"
   1.174  proof -
   1.175 -  have 1: "openin (subtopology euclidean S)
   1.176 -             {b. \<exists>T. openin (subtopology euclidean S) T \<and>
   1.177 +  have 1: "openin (top_of_set S)
   1.178 +             {b. \<exists>T. openin (top_of_set S) T \<and>
   1.179                       b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
   1.180      apply (subst openin_subopen, clarify)
   1.181      apply (rule_tac x=T in exI, auto)
   1.182      done
   1.183 -  have 2: "openin (subtopology euclidean S)
   1.184 -             {b. \<exists>T. openin (subtopology euclidean S) T \<and>
   1.185 +  have 2: "openin (top_of_set S)
   1.186 +             {b. \<exists>T. openin (top_of_set S) T \<and>
   1.187                       b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> \<not> Q x)}"
   1.188      apply (subst openin_subopen, clarify)
   1.189      apply (rule_tac x=T in exI, auto)
   1.190 @@ -1738,9 +1738,9 @@
   1.191    assumes "connected S"
   1.192        and etc: "a \<in> S" "b \<in> S" "P a" "P b"
   1.193        and trans: "\<And>x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z"
   1.194 -      and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
   1.195 +      and opD: "\<And>T a. \<lbrakk>openin (top_of_set S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
   1.196        and opI: "\<And>a. a \<in> S
   1.197 -             \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and>
   1.198 +             \<Longrightarrow> \<exists>T. openin (top_of_set S) T \<and> a \<in> T \<and>
   1.199                       (\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<longrightarrow> R x y)"
   1.200      shows "R a b"
   1.201  proof -
   1.202 @@ -1754,7 +1754,7 @@
   1.203    assumes "connected S"
   1.204        and etc: "a \<in> S" "b \<in> S" "P a"
   1.205        and opI: "\<And>a. a \<in> S
   1.206 -             \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and>
   1.207 +             \<Longrightarrow> \<exists>T. openin (top_of_set S) T \<and> a \<in> T \<and>
   1.208                       (\<forall>x \<in> T. \<forall>y \<in> T. P x \<longrightarrow> P y)"
   1.209      shows "P b"
   1.210  apply (rule connected_induction [OF \<open>connected S\<close> _, where P = "\<lambda>x. True"], blast)
   1.211 @@ -1767,7 +1767,7 @@
   1.212        and etc: "a \<in> S" "b \<in> S"
   1.213        and sym: "\<And>x y. \<lbrakk>R x y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> R y x"
   1.214        and trans: "\<And>x y z. \<lbrakk>R x y; R y z; x \<in> S; y \<in> S; z \<in> S\<rbrakk> \<Longrightarrow> R x z"
   1.215 -      and opI: "\<And>a. a \<in> S \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. R a x)"
   1.216 +      and opI: "\<And>a. a \<in> S \<Longrightarrow> \<exists>T. openin (top_of_set S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. R a x)"
   1.217      shows "R a b"
   1.218  proof -
   1.219    have "\<And>a b c. \<lbrakk>a \<in> S; b \<in> S; c \<in> S; R a b\<rbrakk> \<Longrightarrow> R a c"
   1.220 @@ -1779,7 +1779,7 @@
   1.221  lemma locally_constant_imp_constant:
   1.222    assumes "connected S"
   1.223        and opI: "\<And>a. a \<in> S
   1.224 -             \<Longrightarrow> \<exists>T. openin (subtopology euclidean S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. f x = f a)"
   1.225 +             \<Longrightarrow> \<exists>T. openin (top_of_set S) T \<and> a \<in> T \<and> (\<forall>x \<in> T. f x = f a)"
   1.226      shows "f constant_on S"
   1.227  proof -
   1.228    have "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> f x = f y"
   1.229 @@ -1805,7 +1805,7 @@
   1.230    shows
   1.231      "locally compact s \<longleftrightarrow>
   1.232       (\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
   1.233 -                    openin (subtopology euclidean s) u \<and> compact v)"
   1.234 +                    openin (top_of_set s) u \<and> compact v)"
   1.235       (is "?lhs = ?rhs")
   1.236  proof
   1.237    assume ?lhs
   1.238 @@ -1816,11 +1816,11 @@
   1.239  next
   1.240    assume r [rule_format]: ?rhs
   1.241    have *: "\<exists>u v.
   1.242 -              openin (subtopology euclidean s) u \<and>
   1.243 +              openin (top_of_set s) u \<and>
   1.244                compact v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<inter> T"
   1.245            if "open T" "x \<in> s" "x \<in> T" for x T
   1.246    proof -
   1.247 -    obtain u v where uv: "x \<in> u" "u \<subseteq> v" "v \<subseteq> s" "compact v" "openin (subtopology euclidean s) u"
   1.248 +    obtain u v where uv: "x \<in> u" "u \<subseteq> v" "v \<subseteq> s" "compact v" "openin (top_of_set s) u"
   1.249        using r [OF \<open>x \<in> s\<close>] by auto
   1.250      obtain e where "e>0" and e: "cball x e \<subseteq> T"
   1.251        using open_contains_cball \<open>open T\<close> \<open>x \<in> T\<close> by blast
   1.252 @@ -1842,7 +1842,7 @@
   1.253    fixes s :: "'a :: metric_space set"
   1.254    assumes "locally compact s"
   1.255    obtains u v where "\<And>x. x \<in> s \<Longrightarrow> x \<in> u x \<and> u x \<subseteq> v x \<and> v x \<subseteq> s \<and>
   1.256 -                             openin (subtopology euclidean s) (u x) \<and> compact (v x)"
   1.257 +                             openin (top_of_set s) (u x) \<and> compact (v x)"
   1.258  using assms
   1.259  unfolding locally_compact by metis
   1.260  
   1.261 @@ -1850,7 +1850,7 @@
   1.262    fixes s :: "'a :: heine_borel set"
   1.263    shows "locally compact s \<longleftrightarrow>
   1.264           (\<forall>x \<in> s. \<exists>u. x \<in> u \<and>
   1.265 -                    openin (subtopology euclidean s) u \<and> compact(closure u) \<and> closure u \<subseteq> s)"
   1.266 +                    openin (top_of_set s) u \<and> compact(closure u) \<and> closure u \<subseteq> s)"
   1.267  apply (simp add: locally_compact)
   1.268  apply (intro ball_cong ex_cong refl iffI)
   1.269  apply (metis bounded_subset closure_eq closure_mono compact_eq_bounded_closed dual_order.trans)
   1.270 @@ -1884,21 +1884,21 @@
   1.271    shows "locally compact s \<longleftrightarrow>
   1.272           (\<forall>k. k \<subseteq> s \<and> compact k
   1.273                \<longrightarrow> (\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
   1.274 -                         openin (subtopology euclidean s) u \<and> compact v))"
   1.275 +                         openin (top_of_set s) u \<and> compact v))"
   1.276          (is "?lhs = ?rhs")
   1.277  proof
   1.278    assume ?lhs
   1.279    then obtain u v where
   1.280      uv: "\<And>x. x \<in> s \<Longrightarrow> x \<in> u x \<and> u x \<subseteq> v x \<and> v x \<subseteq> s \<and>
   1.281 -                             openin (subtopology euclidean s) (u x) \<and> compact (v x)"
   1.282 +                             openin (top_of_set s) (u x) \<and> compact (v x)"
   1.283      by (metis locally_compactE)
   1.284 -  have *: "\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> openin (subtopology euclidean s) u \<and> compact v"
   1.285 +  have *: "\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> openin (top_of_set s) u \<and> compact v"
   1.286            if "k \<subseteq> s" "compact k" for k
   1.287    proof -
   1.288 -    have "\<And>C. (\<forall>c\<in>C. openin (subtopology euclidean k) c) \<and> k \<subseteq> \<Union>C \<Longrightarrow>
   1.289 +    have "\<And>C. (\<forall>c\<in>C. openin (top_of_set k) c) \<and> k \<subseteq> \<Union>C \<Longrightarrow>
   1.290                      \<exists>D\<subseteq>C. finite D \<and> k \<subseteq> \<Union>D"
   1.291        using that by (simp add: compact_eq_openin_cover)
   1.292 -    moreover have "\<forall>c \<in> (\<lambda>x. k \<inter> u x) ` k. openin (subtopology euclidean k) c"
   1.293 +    moreover have "\<forall>c \<in> (\<lambda>x. k \<inter> u x) ` k. openin (top_of_set k) c"
   1.294        using that by clarify (metis subsetD inf.absorb_iff2 openin_subset openin_subtopology_Int_subset topspace_euclidean_subtopology uv)
   1.295      moreover have "k \<subseteq> \<Union>((\<lambda>x. k \<inter> u x) ` k)"
   1.296        using that by clarsimp (meson subsetCE uv)
   1.297 @@ -1931,12 +1931,12 @@
   1.298    assumes "open s"
   1.299      shows "locally compact s"
   1.300  proof -
   1.301 -  have *: "\<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> openin (subtopology euclidean s) u \<and> compact v"
   1.302 +  have *: "\<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> openin (top_of_set s) u \<and> compact v"
   1.303            if "x \<in> s" for x
   1.304    proof -
   1.305      obtain e where "e>0" and e: "cball x e \<subseteq> s"
   1.306        using open_contains_cball assms \<open>x \<in> s\<close> by blast
   1.307 -    have ope: "openin (subtopology euclidean s) (ball x e)"
   1.308 +    have ope: "openin (top_of_set s) (ball x e)"
   1.309        by (meson e open_ball ball_subset_cball dual_order.trans open_subset)
   1.310      show ?thesis
   1.311        apply (rule_tac x="ball x e" in exI)
   1.312 @@ -1955,7 +1955,7 @@
   1.313      shows "locally compact s"
   1.314  proof -
   1.315    have *: "\<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
   1.316 -                 openin (subtopology euclidean s) u \<and> compact v"
   1.317 +                 openin (top_of_set s) u \<and> compact v"
   1.318            if "x \<in> s" for x
   1.319    proof -
   1.320      show ?thesis
   1.321 @@ -1979,7 +1979,7 @@
   1.322  
   1.323  lemma locally_compact_closedin:
   1.324    fixes s :: "'a :: heine_borel set"
   1.325 -  shows "\<lbrakk>closedin (subtopology euclidean s) t; locally compact s\<rbrakk>
   1.326 +  shows "\<lbrakk>closedin (top_of_set s) t; locally compact s\<rbrakk>
   1.327          \<Longrightarrow> locally compact t"
   1.328  unfolding closedin_closed
   1.329  using closed_imp_locally_compact locally_compact_Int by blast
   1.330 @@ -2010,8 +2010,8 @@
   1.331  lemma locally_compact_openin_Un:
   1.332    fixes S :: "'a::euclidean_space set"
   1.333    assumes LCS: "locally compact S" and LCT:"locally compact T"
   1.334 -      and opS: "openin (subtopology euclidean (S \<union> T)) S"
   1.335 -      and opT: "openin (subtopology euclidean (S \<union> T)) T"
   1.336 +      and opS: "openin (top_of_set (S \<union> T)) S"
   1.337 +      and opT: "openin (top_of_set (S \<union> T)) T"
   1.338      shows "locally compact (S \<union> T)"
   1.339  proof -
   1.340    have "\<exists>e>0. closed (cball x e \<inter> (S \<union> T))" if "x \<in> S" for x
   1.341 @@ -2047,8 +2047,8 @@
   1.342  lemma locally_compact_closedin_Un:
   1.343    fixes S :: "'a::euclidean_space set"
   1.344    assumes LCS: "locally compact S" and LCT:"locally compact T"
   1.345 -      and clS: "closedin (subtopology euclidean (S \<union> T)) S"
   1.346 -      and clT: "closedin (subtopology euclidean (S \<union> T)) T"
   1.347 +      and clS: "closedin (top_of_set (S \<union> T)) S"
   1.348 +      and clT: "closedin (top_of_set (S \<union> T)) T"
   1.349      shows "locally compact (S \<union> T)"
   1.350  proof -
   1.351    have "\<exists>e>0. closed (cball x e \<inter> (S \<union> T))" if "x \<in> S" "x \<in> T" for x
   1.352 @@ -2113,7 +2113,7 @@
   1.353     "locally compact S \<longleftrightarrow>
   1.354      (\<forall>K T. K \<subseteq> S \<and> compact K \<and> open T \<and> K \<subseteq> T
   1.355            \<longrightarrow> (\<exists>U V. K \<subseteq> U \<and> U \<subseteq> V \<and> U \<subseteq> T \<and> V \<subseteq> S \<and>
   1.356 -                     openin (subtopology euclidean S) U \<and> compact V))"
   1.357 +                     openin (top_of_set S) U \<and> compact V))"
   1.358     (is "?lhs = ?rhs")
   1.359  proof
   1.360    assume L: ?lhs
   1.361 @@ -2122,10 +2122,10 @@
   1.362      fix K :: "'a set" and T :: "'a set"
   1.363      assume "K \<subseteq> S" and "compact K" and "open T" and "K \<subseteq> T"
   1.364      obtain U V where "K \<subseteq> U" "U \<subseteq> V" "V \<subseteq> S" "compact V"
   1.365 -                 and ope: "openin (subtopology euclidean S) U"
   1.366 +                 and ope: "openin (top_of_set S) U"
   1.367        using L unfolding locally_compact_compact by (meson \<open>K \<subseteq> S\<close> \<open>compact K\<close>)
   1.368      show "\<exists>U V. K \<subseteq> U \<and> U \<subseteq> V \<and> U \<subseteq> T \<and> V \<subseteq> S \<and>
   1.369 -                openin (subtopology euclidean S) U \<and> compact V"
   1.370 +                openin (top_of_set S) U \<and> compact V"
   1.371      proof (intro exI conjI)
   1.372        show "K \<subseteq> U \<inter> T"
   1.373          by (simp add: \<open>K \<subseteq> T\<close> \<open>K \<subseteq> U\<close>)
   1.374 @@ -2133,7 +2133,7 @@
   1.375          by (rule closure_subset)
   1.376        show "closure (U \<inter> T) \<subseteq> S"
   1.377          by (metis \<open>U \<subseteq> V\<close> \<open>V \<subseteq> S\<close> \<open>compact V\<close> closure_closed closure_mono compact_imp_closed inf.cobounded1 subset_trans)
   1.378 -      show "openin (subtopology euclidean S) (U \<inter> T)"
   1.379 +      show "openin (top_of_set S) (U \<inter> T)"
   1.380          by (simp add: \<open>open T\<close> ope openin_Int_open)
   1.381        show "compact (closure (U \<inter> T))"
   1.382          by (meson Int_lower1 \<open>U \<subseteq> V\<close> \<open>compact V\<close> bounded_subset compact_closure compact_eq_bounded_closed)
   1.383 @@ -2151,8 +2151,8 @@
   1.384  proposition Sura_Bura_compact:
   1.385    fixes S :: "'a::euclidean_space set"
   1.386    assumes "compact S" and C: "C \<in> components S"
   1.387 -  shows "C = \<Inter>{T. C \<subseteq> T \<and> openin (subtopology euclidean S) T \<and>
   1.388 -                           closedin (subtopology euclidean S) T}"
   1.389 +  shows "C = \<Inter>{T. C \<subseteq> T \<and> openin (top_of_set S) T \<and>
   1.390 +                           closedin (top_of_set S) T}"
   1.391           (is "C = \<Inter>?\<T>")
   1.392  proof
   1.393    obtain x where x: "C = connected_component_set S x" and "x \<in> S"
   1.394 @@ -2168,8 +2168,8 @@
   1.395      have clo: "closed (\<Inter>?\<T>)"
   1.396        by (simp add: \<open>compact S\<close> closed_Inter closedin_compact_eq compact_imp_closed)
   1.397      have False
   1.398 -      if K1: "closedin (subtopology euclidean (\<Inter>?\<T>)) K1" and
   1.399 -         K2: "closedin (subtopology euclidean (\<Inter>?\<T>)) K2" and
   1.400 +      if K1: "closedin (top_of_set (\<Inter>?\<T>)) K1" and
   1.401 +         K2: "closedin (top_of_set (\<Inter>?\<T>)) K2" and
   1.402           K12_Int: "K1 \<inter> K2 = {}" and K12_Un: "K1 \<union> K2 = \<Inter>?\<T>" and "K1 \<noteq> {}" "K2 \<noteq> {}"
   1.403         for K1 K2
   1.404      proof -
   1.405 @@ -2187,8 +2187,8 @@
   1.406          show "(S - (V1 \<union> V2)) \<inter> \<Inter>\<F> \<noteq> {}" if "finite \<F>" and \<F>: "\<F> \<subseteq> ?\<T>" for \<F>
   1.407          proof
   1.408            assume djo: "(S - (V1 \<union> V2)) \<inter> \<Inter>\<F> = {}"
   1.409 -          obtain D where opeD: "openin (subtopology euclidean S) D"
   1.410 -                   and cloD: "closedin (subtopology euclidean S) D"
   1.411 +          obtain D where opeD: "openin (top_of_set S) D"
   1.412 +                   and cloD: "closedin (top_of_set S) D"
   1.413                     and "C \<subseteq> D" and DV12: "D \<subseteq> V1 \<union> V2"
   1.414            proof (cases "\<F> = {}")
   1.415              case True
   1.416 @@ -2197,9 +2197,9 @@
   1.417            next
   1.418              case False show ?thesis
   1.419              proof
   1.420 -              show ope: "openin (subtopology euclidean S) (\<Inter>\<F>)"
   1.421 +              show ope: "openin (top_of_set S) (\<Inter>\<F>)"
   1.422                  using openin_Inter \<open>finite \<F>\<close> False \<F> by blast
   1.423 -              then show "closedin (subtopology euclidean S) (\<Inter>\<F>)"
   1.424 +              then show "closedin (top_of_set S) (\<Inter>\<F>)"
   1.425                  by (meson clo\<T> \<F> closed_Inter closed_subset openin_imp_subset subset_eq)
   1.426                show "C \<subseteq> \<Inter>\<F>"
   1.427                  using \<F> by auto
   1.428 @@ -2211,16 +2211,16 @@
   1.429              by (simp add: x)
   1.430            have "closed D"
   1.431              using \<open>compact S\<close> cloD closedin_closed_trans compact_imp_closed by blast
   1.432 -          have cloV1: "closedin (subtopology euclidean D) (D \<inter> closure V1)"
   1.433 -            and cloV2: "closedin (subtopology euclidean D) (D \<inter> closure V2)"
   1.434 +          have cloV1: "closedin (top_of_set D) (D \<inter> closure V1)"
   1.435 +            and cloV2: "closedin (top_of_set D) (D \<inter> closure V2)"
   1.436              by (simp_all add: closedin_closed_Int)
   1.437            moreover have "D \<inter> closure V1 = D \<inter> V1" "D \<inter> closure V2 = D \<inter> V2"
   1.438              apply safe
   1.439              using \<open>D \<subseteq> V1 \<union> V2\<close> \<open>open V1\<close> \<open>open V2\<close> V12
   1.440                 apply (simp_all add: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
   1.441              done
   1.442 -          ultimately have cloDV1: "closedin (subtopology euclidean D) (D \<inter> V1)"
   1.443 -                      and cloDV2:  "closedin (subtopology euclidean D) (D \<inter> V2)"
   1.444 +          ultimately have cloDV1: "closedin (top_of_set D) (D \<inter> V1)"
   1.445 +                      and cloDV2:  "closedin (top_of_set D) (D \<inter> V2)"
   1.446              by metis+
   1.447            then obtain U1 U2 where "closed U1" "closed U2"
   1.448                 and D1: "D \<inter> V1 = D \<inter> U1" and D2: "D \<inter> V2 = D \<inter> U2"
   1.449 @@ -2274,21 +2274,21 @@
   1.450    fixes S :: "'a::euclidean_space set"
   1.451    assumes S: "locally compact S" and C: "C \<in> components S" and "compact C"
   1.452        and U: "open U" "C \<subseteq> U"
   1.453 -  obtains K where "openin (subtopology euclidean S) K" "compact K" "C \<subseteq> K" "K \<subseteq> U"
   1.454 +  obtains K where "openin (top_of_set S) K" "compact K" "C \<subseteq> K" "K \<subseteq> U"
   1.455  proof (rule ccontr)
   1.456    assume "\<not> thesis"
   1.457 -  with that have neg: "\<nexists>K. openin (subtopology euclidean S) K \<and> compact K \<and> C \<subseteq> K \<and> K \<subseteq> U"
   1.458 +  with that have neg: "\<nexists>K. openin (top_of_set S) K \<and> compact K \<and> C \<subseteq> K \<and> K \<subseteq> U"
   1.459      by metis
   1.460    obtain V K where "C \<subseteq> V" "V \<subseteq> U" "V \<subseteq> K" "K \<subseteq> S" "compact K"
   1.461 -               and opeSV: "openin (subtopology euclidean S) V"
   1.462 +               and opeSV: "openin (top_of_set S) V"
   1.463      using S U \<open>compact C\<close>
   1.464      apply (simp add: locally_compact_compact_subopen)
   1.465      by (meson C in_components_subset)
   1.466 -  let ?\<T> = "{T. C \<subseteq> T \<and> openin (subtopology euclidean K) T \<and> compact T \<and> T \<subseteq> K}"
   1.467 +  let ?\<T> = "{T. C \<subseteq> T \<and> openin (top_of_set K) T \<and> compact T \<and> T \<subseteq> K}"
   1.468    have CK: "C \<in> components K"
   1.469      by (meson C \<open>C \<subseteq> V\<close> \<open>K \<subseteq> S\<close> \<open>V \<subseteq> K\<close> components_intermediate_subset subset_trans)
   1.470    with \<open>compact K\<close>
   1.471 -  have "C = \<Inter>{T. C \<subseteq> T \<and> openin (subtopology euclidean K) T \<and> closedin (subtopology euclidean K) T}"
   1.472 +  have "C = \<Inter>{T. C \<subseteq> T \<and> openin (top_of_set K) T \<and> closedin (top_of_set K) T}"
   1.473      by (simp add: Sura_Bura_compact)
   1.474    then have Ceq: "C = \<Inter>?\<T>"
   1.475      by (simp add: closedin_compact_eq \<open>compact K\<close>)
   1.476 @@ -2322,11 +2322,11 @@
   1.477            by (metis (no_types, lifting) compact_Inter False mem_Collect_eq subsetCE \<F>)
   1.478          moreover have "\<Inter>\<F> \<subseteq> K"
   1.479            using False that(2) by fastforce
   1.480 -        moreover have opeKF: "openin (subtopology euclidean K) (\<Inter>\<F>)"
   1.481 +        moreover have opeKF: "openin (top_of_set K) (\<Inter>\<F>)"
   1.482            using False \<F> \<open>finite \<F>\<close> by blast
   1.483 -        then have opeVF: "openin (subtopology euclidean V) (\<Inter>\<F>)"
   1.484 +        then have opeVF: "openin (top_of_set V) (\<Inter>\<F>)"
   1.485            using W \<open>K \<subseteq> S\<close> \<open>V \<subseteq> K\<close> opeKF \<open>\<Inter>\<F> \<subseteq> K\<close> FUW openin_subset_trans by fastforce
   1.486 -        then have "openin (subtopology euclidean S) (\<Inter>\<F>)"
   1.487 +        then have "openin (top_of_set S) (\<Inter>\<F>)"
   1.488            by (metis opeSV openin_trans)
   1.489          moreover have "\<Inter>\<F> \<subseteq> U"
   1.490            by (meson \<open>V \<subseteq> U\<close> opeVF dual_order.trans openin_imp_subset)
   1.491 @@ -2343,8 +2343,8 @@
   1.492  corollary Sura_Bura_clopen_subset_alt:
   1.493    fixes S :: "'a::euclidean_space set"
   1.494    assumes S: "locally compact S" and C: "C \<in> components S" and "compact C"
   1.495 -      and opeSU: "openin (subtopology euclidean S) U" and "C \<subseteq> U"
   1.496 -  obtains K where "openin (subtopology euclidean S) K" "compact K" "C \<subseteq> K" "K \<subseteq> U"
   1.497 +      and opeSU: "openin (top_of_set S) U" and "C \<subseteq> U"
   1.498 +  obtains K where "openin (top_of_set S) K" "compact K" "C \<subseteq> K" "K \<subseteq> U"
   1.499  proof -
   1.500    obtain V where "open V" "U = S \<inter> V"
   1.501      using opeSU by (auto simp: openin_open)
   1.502 @@ -2358,13 +2358,13 @@
   1.503  corollary Sura_Bura:
   1.504    fixes S :: "'a::euclidean_space set"
   1.505    assumes "locally compact S" "C \<in> components S" "compact C"
   1.506 -  shows "C = \<Inter> {K. C \<subseteq> K \<and> compact K \<and> openin (subtopology euclidean S) K}"
   1.507 +  shows "C = \<Inter> {K. C \<subseteq> K \<and> compact K \<and> openin (top_of_set S) K}"
   1.508           (is "C = ?rhs")
   1.509  proof
   1.510    show "?rhs \<subseteq> C"
   1.511    proof (clarsimp, rule ccontr)
   1.512      fix x
   1.513 -    assume *: "\<forall>X. C \<subseteq> X \<and> compact X \<and> openin (subtopology euclidean S) X \<longrightarrow> x \<in> X"
   1.514 +    assume *: "\<forall>X. C \<subseteq> X \<and> compact X \<and> openin (top_of_set S) X \<longrightarrow> x \<in> X"
   1.515        and "x \<notin> C"
   1.516      obtain U V where "open U" "open V" "{x} \<subseteq> U" "C \<subseteq> V" "U \<inter> V = {}"
   1.517        using separation_normal [of "{x}" C]
   1.518 @@ -2381,8 +2381,8 @@
   1.519  
   1.520  lemma locally_connected_1:
   1.521    assumes
   1.522 -    "\<And>v x. \<lbrakk>openin (subtopology euclidean S) v; x \<in> v\<rbrakk>
   1.523 -              \<Longrightarrow> \<exists>u. openin (subtopology euclidean S) u \<and>
   1.524 +    "\<And>v x. \<lbrakk>openin (top_of_set S) v; x \<in> v\<rbrakk>
   1.525 +              \<Longrightarrow> \<exists>u. openin (top_of_set S) u \<and>
   1.526                        connected u \<and> x \<in> u \<and> u \<subseteq> v"
   1.527     shows "locally connected S"
   1.528  apply (clarsimp simp add: locally_def)
   1.529 @@ -2391,12 +2391,12 @@
   1.530  
   1.531  lemma locally_connected_2:
   1.532    assumes "locally connected S"
   1.533 -          "openin (subtopology euclidean S) t"
   1.534 +          "openin (top_of_set S) t"
   1.535            "x \<in> t"
   1.536 -   shows "openin (subtopology euclidean S) (connected_component_set t x)"
   1.537 +   shows "openin (top_of_set S) (connected_component_set t x)"
   1.538  proof -
   1.539    { fix y :: 'a
   1.540 -    let ?SS = "subtopology euclidean S"
   1.541 +    let ?SS = "top_of_set S"
   1.542      assume 1: "openin ?SS t"
   1.543                "\<forall>w x. openin ?SS w \<and> x \<in> w \<longrightarrow> (\<exists>u. openin ?SS u \<and> (\<exists>v. connected v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w))"
   1.544      and "connected_component t x y"
   1.545 @@ -2420,29 +2420,29 @@
   1.546  qed
   1.547  
   1.548  lemma locally_connected_3:
   1.549 -  assumes "\<And>t x. \<lbrakk>openin (subtopology euclidean S) t; x \<in> t\<rbrakk>
   1.550 -              \<Longrightarrow> openin (subtopology euclidean S)
   1.551 +  assumes "\<And>t x. \<lbrakk>openin (top_of_set S) t; x \<in> t\<rbrakk>
   1.552 +              \<Longrightarrow> openin (top_of_set S)
   1.553                            (connected_component_set t x)"
   1.554 -          "openin (subtopology euclidean S) v" "x \<in> v"
   1.555 -   shows  "\<exists>u. openin (subtopology euclidean S) u \<and> connected u \<and> x \<in> u \<and> u \<subseteq> v"
   1.556 +          "openin (top_of_set S) v" "x \<in> v"
   1.557 +   shows  "\<exists>u. openin (top_of_set S) u \<and> connected u \<and> x \<in> u \<and> u \<subseteq> v"
   1.558  using assms connected_component_subset by fastforce
   1.559  
   1.560  lemma locally_connected:
   1.561    "locally connected S \<longleftrightarrow>
   1.562 -   (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
   1.563 -          \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> connected u \<and> x \<in> u \<and> u \<subseteq> v))"
   1.564 +   (\<forall>v x. openin (top_of_set S) v \<and> x \<in> v
   1.565 +          \<longrightarrow> (\<exists>u. openin (top_of_set S) u \<and> connected u \<and> x \<in> u \<and> u \<subseteq> v))"
   1.566  by (metis locally_connected_1 locally_connected_2 locally_connected_3)
   1.567  
   1.568  lemma locally_connected_open_connected_component:
   1.569    "locally connected S \<longleftrightarrow>
   1.570 -   (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
   1.571 -          \<longrightarrow> openin (subtopology euclidean S) (connected_component_set t x))"
   1.572 +   (\<forall>t x. openin (top_of_set S) t \<and> x \<in> t
   1.573 +          \<longrightarrow> openin (top_of_set S) (connected_component_set t x))"
   1.574  by (metis locally_connected_1 locally_connected_2 locally_connected_3)
   1.575  
   1.576  lemma locally_path_connected_1:
   1.577    assumes
   1.578 -    "\<And>v x. \<lbrakk>openin (subtopology euclidean S) v; x \<in> v\<rbrakk>
   1.579 -              \<Longrightarrow> \<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v"
   1.580 +    "\<And>v x. \<lbrakk>openin (top_of_set S) v; x \<in> v\<rbrakk>
   1.581 +              \<Longrightarrow> \<exists>u. openin (top_of_set S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v"
   1.582     shows "locally path_connected S"
   1.583  apply (clarsimp simp add: locally_def)
   1.584  apply (drule assms; blast)
   1.585 @@ -2450,12 +2450,12 @@
   1.586  
   1.587  lemma locally_path_connected_2:
   1.588    assumes "locally path_connected S"
   1.589 -          "openin (subtopology euclidean S) t"
   1.590 +          "openin (top_of_set S) t"
   1.591            "x \<in> t"
   1.592 -   shows "openin (subtopology euclidean S) (path_component_set t x)"
   1.593 +   shows "openin (top_of_set S) (path_component_set t x)"
   1.594  proof -
   1.595    { fix y :: 'a
   1.596 -    let ?SS = "subtopology euclidean S"
   1.597 +    let ?SS = "top_of_set S"
   1.598      assume 1: "openin ?SS t"
   1.599                "\<forall>w x. openin ?SS w \<and> x \<in> w \<longrightarrow> (\<exists>u. openin ?SS u \<and> (\<exists>v. path_connected v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w))"
   1.600      and "path_component t x y"
   1.601 @@ -2479,10 +2479,10 @@
   1.602  qed
   1.603  
   1.604  lemma locally_path_connected_3:
   1.605 -  assumes "\<And>t x. \<lbrakk>openin (subtopology euclidean S) t; x \<in> t\<rbrakk>
   1.606 -              \<Longrightarrow> openin (subtopology euclidean S) (path_component_set t x)"
   1.607 -          "openin (subtopology euclidean S) v" "x \<in> v"
   1.608 -   shows  "\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v"
   1.609 +  assumes "\<And>t x. \<lbrakk>openin (top_of_set S) t; x \<in> t\<rbrakk>
   1.610 +              \<Longrightarrow> openin (top_of_set S) (path_component_set t x)"
   1.611 +          "openin (top_of_set S) v" "x \<in> v"
   1.612 +   shows  "\<exists>u. openin (top_of_set S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v"
   1.613  proof -
   1.614    have "path_component v x x"
   1.615      by (meson assms(3) path_component_refl)
   1.616 @@ -2492,26 +2492,26 @@
   1.617  
   1.618  proposition locally_path_connected:
   1.619    "locally path_connected S \<longleftrightarrow>
   1.620 -   (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
   1.621 -          \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))"
   1.622 +   (\<forall>v x. openin (top_of_set S) v \<and> x \<in> v
   1.623 +          \<longrightarrow> (\<exists>u. openin (top_of_set S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))"
   1.624    by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
   1.625  
   1.626  proposition locally_path_connected_open_path_component:
   1.627    "locally path_connected S \<longleftrightarrow>
   1.628 -   (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
   1.629 -          \<longrightarrow> openin (subtopology euclidean S) (path_component_set t x))"
   1.630 +   (\<forall>t x. openin (top_of_set S) t \<and> x \<in> t
   1.631 +          \<longrightarrow> openin (top_of_set S) (path_component_set t x))"
   1.632    by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
   1.633  
   1.634  lemma locally_connected_open_component:
   1.635    "locally connected S \<longleftrightarrow>
   1.636 -   (\<forall>t c. openin (subtopology euclidean S) t \<and> c \<in> components t
   1.637 -          \<longrightarrow> openin (subtopology euclidean S) c)"
   1.638 +   (\<forall>t c. openin (top_of_set S) t \<and> c \<in> components t
   1.639 +          \<longrightarrow> openin (top_of_set S) c)"
   1.640  by (metis components_iff locally_connected_open_connected_component)
   1.641  
   1.642  proposition locally_connected_im_kleinen:
   1.643    "locally connected S \<longleftrightarrow>
   1.644 -   (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
   1.645 -       \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
   1.646 +   (\<forall>v x. openin (top_of_set S) v \<and> x \<in> v
   1.647 +       \<longrightarrow> (\<exists>u. openin (top_of_set S) u \<and>
   1.648                  x \<in> u \<and> u \<subseteq> v \<and>
   1.649                  (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> v \<and> x \<in> c \<and> y \<in> c))))"
   1.650     (is "?lhs = ?rhs")
   1.651 @@ -2521,12 +2521,12 @@
   1.652      by (fastforce simp add: locally_connected)
   1.653  next
   1.654    assume ?rhs
   1.655 -  have *: "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> c"
   1.656 -       if "openin (subtopology euclidean S) t" and c: "c \<in> components t" and "x \<in> c" for t c x
   1.657 +  have *: "\<exists>T. openin (top_of_set S) T \<and> x \<in> T \<and> T \<subseteq> c"
   1.658 +       if "openin (top_of_set S) t" and c: "c \<in> components t" and "x \<in> c" for t c x
   1.659    proof -
   1.660      from that \<open>?rhs\<close> [rule_format, of t x]
   1.661      obtain u where u:
   1.662 -      "openin (subtopology euclidean S) u \<and> x \<in> u \<and> u \<subseteq> t \<and>
   1.663 +      "openin (top_of_set S) u \<and> x \<in> u \<and> u \<subseteq> t \<and>
   1.664         (\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> t \<and> x \<in> c \<and> y \<in> c))"
   1.665        using in_components_subset by auto
   1.666      obtain F :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a" where
   1.667 @@ -2551,8 +2551,8 @@
   1.668  
   1.669  proposition locally_path_connected_im_kleinen:
   1.670    "locally path_connected S \<longleftrightarrow>
   1.671 -   (\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
   1.672 -       \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
   1.673 +   (\<forall>v x. openin (top_of_set S) v \<and> x \<in> v
   1.674 +       \<longrightarrow> (\<exists>u. openin (top_of_set S) u \<and>
   1.675                  x \<in> u \<and> u \<subseteq> v \<and>
   1.676                  (\<forall>y. y \<in> u \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> v \<and>
   1.677                                  pathstart p = x \<and> pathfinish p = y))))"
   1.678 @@ -2565,15 +2565,15 @@
   1.679      by (meson dual_order.trans)
   1.680  next
   1.681    assume ?rhs
   1.682 -  have *: "\<exists>T. openin (subtopology euclidean S) T \<and>
   1.683 +  have *: "\<exists>T. openin (top_of_set S) T \<and>
   1.684                 x \<in> T \<and> T \<subseteq> path_component_set u z"
   1.685 -       if "openin (subtopology euclidean S) u" and "z \<in> u" and c: "path_component u z x" for u z x
   1.686 +       if "openin (top_of_set S) u" and "z \<in> u" and c: "path_component u z x" for u z x
   1.687    proof -
   1.688      have "x \<in> u"
   1.689        by (meson c path_component_mem(2))
   1.690      with that \<open>?rhs\<close> [rule_format, of u x]
   1.691      obtain U where U:
   1.692 -      "openin (subtopology euclidean S) U \<and> x \<in> U \<and> U \<subseteq> u \<and>
   1.693 +      "openin (top_of_set S) U \<and> x \<in> U \<and> U \<subseteq> u \<and>
   1.694         (\<forall>y. y \<in> U \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> u \<and> pathstart p = x \<and> pathfinish p = y))"
   1.695         by blast
   1.696      show ?thesis
   1.697 @@ -2626,22 +2626,22 @@
   1.698  
   1.699  lemma openin_connected_component_locally_connected:
   1.700      "locally connected S
   1.701 -     \<Longrightarrow> openin (subtopology euclidean S) (connected_component_set S x)"
   1.702 +     \<Longrightarrow> openin (top_of_set S) (connected_component_set S x)"
   1.703  apply (simp add: locally_connected_open_connected_component)
   1.704  by (metis connected_component_eq_empty connected_component_subset open_empty open_subset openin_subtopology_self)
   1.705  
   1.706  lemma openin_components_locally_connected:
   1.707 -    "\<lbrakk>locally connected S; c \<in> components S\<rbrakk> \<Longrightarrow> openin (subtopology euclidean S) c"
   1.708 +    "\<lbrakk>locally connected S; c \<in> components S\<rbrakk> \<Longrightarrow> openin (top_of_set S) c"
   1.709    using locally_connected_open_component openin_subtopology_self by blast
   1.710  
   1.711  lemma openin_path_component_locally_path_connected:
   1.712    "locally path_connected S
   1.713 -        \<Longrightarrow> openin (subtopology euclidean S) (path_component_set S x)"
   1.714 +        \<Longrightarrow> openin (top_of_set S) (path_component_set S x)"
   1.715  by (metis (no_types) empty_iff locally_path_connected_2 openin_subopen openin_subtopology_self path_component_eq_empty)
   1.716  
   1.717  lemma closedin_path_component_locally_path_connected:
   1.718      "locally path_connected S
   1.719 -        \<Longrightarrow> closedin (subtopology euclidean S) (path_component_set S x)"
   1.720 +        \<Longrightarrow> closedin (top_of_set S) (path_component_set S x)"
   1.721  apply  (simp add: closedin_def path_component_subset complement_path_component_Union)
   1.722  apply (rule openin_Union)
   1.723  using openin_path_component_locally_path_connected by auto
   1.724 @@ -2670,12 +2670,12 @@
   1.725      shows "(path_component S x = connected_component S x)"
   1.726  proof (cases "x \<in> S")
   1.727    case True
   1.728 -  have "openin (subtopology euclidean (connected_component_set S x)) (path_component_set S x)"
   1.729 +  have "openin (top_of_set (connected_component_set S x)) (path_component_set S x)"
   1.730      apply (rule openin_subset_trans [of S])
   1.731      apply (intro conjI openin_path_component_locally_path_connected [OF assms])
   1.732      using path_component_subset_connected_component   apply (auto simp: connected_component_subset)
   1.733      done
   1.734 -  moreover have "closedin (subtopology euclidean (connected_component_set S x)) (path_component_set S x)"
   1.735 +  moreover have "closedin (top_of_set (connected_component_set S x)) (path_component_set S x)"
   1.736      apply (rule closedin_subset_trans [of S])
   1.737      apply (intro conjI closedin_path_component_locally_path_connected [OF assms])
   1.738      using path_component_subset_connected_component   apply (auto simp: connected_component_subset)
   1.739 @@ -2710,26 +2710,26 @@
   1.740  proposition locally_connected_quotient_image:
   1.741    assumes lcS: "locally connected S"
   1.742        and oo: "\<And>T. T \<subseteq> f ` S
   1.743 -                \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
   1.744 -                    openin (subtopology euclidean (f ` S)) T"
   1.745 +                \<Longrightarrow> openin (top_of_set S) (S \<inter> f -` T) \<longleftrightarrow>
   1.746 +                    openin (top_of_set (f ` S)) T"
   1.747      shows "locally connected (f ` S)"
   1.748  proof (clarsimp simp: locally_connected_open_component)
   1.749    fix U C
   1.750 -  assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "C \<in> components U"
   1.751 +  assume opefSU: "openin (top_of_set (f ` S)) U" and "C \<in> components U"
   1.752    then have "C \<subseteq> U" "U \<subseteq> f ` S"
   1.753      by (meson in_components_subset openin_imp_subset)+
   1.754 -  then have "openin (subtopology euclidean (f ` S)) C \<longleftrightarrow>
   1.755 -             openin (subtopology euclidean S) (S \<inter> f -` C)"
   1.756 +  then have "openin (top_of_set (f ` S)) C \<longleftrightarrow>
   1.757 +             openin (top_of_set S) (S \<inter> f -` C)"
   1.758      by (auto simp: oo)
   1.759 -  moreover have "openin (subtopology euclidean S) (S \<inter> f -` C)"
   1.760 +  moreover have "openin (top_of_set S) (S \<inter> f -` C)"
   1.761    proof (subst openin_subopen, clarify)
   1.762      fix x
   1.763      assume "x \<in> S" "f x \<in> C"
   1.764 -    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> (S \<inter> f -` C)"
   1.765 +    show "\<exists>T. openin (top_of_set S) T \<and> x \<in> T \<and> T \<subseteq> (S \<inter> f -` C)"
   1.766      proof (intro conjI exI)
   1.767 -      show "openin (subtopology euclidean S) (connected_component_set (S \<inter> f -` U) x)"
   1.768 +      show "openin (top_of_set S) (connected_component_set (S \<inter> f -` U) x)"
   1.769        proof (rule ccontr)
   1.770 -        assume **: "\<not> openin (subtopology euclidean S) (connected_component_set (S \<inter> f -` U) x)"
   1.771 +        assume **: "\<not> openin (top_of_set S) (connected_component_set (S \<inter> f -` U) x)"
   1.772          then have "x \<notin> (S \<inter> f -` U)"
   1.773            using \<open>U \<subseteq> f ` S\<close> opefSU lcS locally_connected_2 oo by blast
   1.774          with ** show False
   1.775 @@ -2768,7 +2768,7 @@
   1.776        finally show "connected_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` C)" .
   1.777      qed
   1.778    qed
   1.779 -  ultimately show "openin (subtopology euclidean (f ` S)) C"
   1.780 +  ultimately show "openin (top_of_set (f ` S)) C"
   1.781      by metis
   1.782  qed
   1.783  
   1.784 @@ -2776,32 +2776,32 @@
   1.785  proposition locally_path_connected_quotient_image:
   1.786    assumes lcS: "locally path_connected S"
   1.787        and oo: "\<And>T. T \<subseteq> f ` S
   1.788 -                \<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> openin (subtopology euclidean (f ` S)) T"
   1.789 +                \<Longrightarrow> openin (top_of_set S) (S \<inter> f -` T) \<longleftrightarrow> openin (top_of_set (f ` S)) T"
   1.790      shows "locally path_connected (f ` S)"
   1.791  proof (clarsimp simp: locally_path_connected_open_path_component)
   1.792    fix U y
   1.793 -  assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "y \<in> U"
   1.794 +  assume opefSU: "openin (top_of_set (f ` S)) U" and "y \<in> U"
   1.795    then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
   1.796      by (meson path_component_subset openin_imp_subset)+
   1.797 -  then have "openin (subtopology euclidean (f ` S)) (path_component_set U y) \<longleftrightarrow>
   1.798 -             openin (subtopology euclidean S) (S \<inter> f -` path_component_set U y)"
   1.799 +  then have "openin (top_of_set (f ` S)) (path_component_set U y) \<longleftrightarrow>
   1.800 +             openin (top_of_set S) (S \<inter> f -` path_component_set U y)"
   1.801    proof -
   1.802      have "path_component_set U y \<subseteq> f ` S"
   1.803        using \<open>U \<subseteq> f ` S\<close> \<open>path_component_set U y \<subseteq> U\<close> by blast
   1.804      then show ?thesis
   1.805        using oo by blast
   1.806    qed
   1.807 -  moreover have "openin (subtopology euclidean S) (S \<inter> f -` path_component_set U y)"
   1.808 +  moreover have "openin (top_of_set S) (S \<inter> f -` path_component_set U y)"
   1.809    proof (subst openin_subopen, clarify)
   1.810      fix x
   1.811      assume "x \<in> S" and Uyfx: "path_component U y (f x)"
   1.812      then have "f x \<in> U"
   1.813        using path_component_mem by blast
   1.814 -    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> (S \<inter> f -` path_component_set U y)"
   1.815 +    show "\<exists>T. openin (top_of_set S) T \<and> x \<in> T \<and> T \<subseteq> (S \<inter> f -` path_component_set U y)"
   1.816      proof (intro conjI exI)
   1.817 -      show "openin (subtopology euclidean S) (path_component_set (S \<inter> f -` U) x)"
   1.818 +      show "openin (top_of_set S) (path_component_set (S \<inter> f -` U) x)"
   1.819        proof (rule ccontr)
   1.820 -        assume **: "\<not> openin (subtopology euclidean S) (path_component_set (S \<inter> f -` U) x)"
   1.821 +        assume **: "\<not> openin (top_of_set S) (path_component_set (S \<inter> f -` U) x)"
   1.822          then have "x \<notin> (S \<inter> f -` U)"
   1.823            by (metis (no_types, lifting) \<open>U \<subseteq> f ` S\<close> opefSU lcS oo locally_path_connected_open_path_component)
   1.824          then show False
   1.825 @@ -2842,7 +2842,7 @@
   1.826        finally show "path_component_set (S \<inter> f -` U) x \<subseteq> (S \<inter> f -` path_component_set U y)" .
   1.827      qed
   1.828    qed
   1.829 -  ultimately show "openin (subtopology euclidean (f ` S)) (path_component_set U y)"
   1.830 +  ultimately show "openin (top_of_set (f ` S)) (path_component_set U y)"
   1.831      by metis
   1.832  qed
   1.833  
   1.834 @@ -2851,14 +2851,14 @@
   1.835  lemma continuous_on_components_gen:
   1.836   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   1.837    assumes "\<And>c. c \<in> components S \<Longrightarrow>
   1.838 -              openin (subtopology euclidean S) c \<and> continuous_on c f"
   1.839 +              openin (top_of_set S) c \<and> continuous_on c f"
   1.840      shows "continuous_on S f"
   1.841  proof (clarsimp simp: continuous_openin_preimage_eq)
   1.842    fix t :: "'b set"
   1.843    assume "open t"
   1.844    have *: "S \<inter> f -` t = (\<Union>c \<in> components S. c \<inter> f -` t)"
   1.845      by auto
   1.846 -  show "openin (subtopology euclidean S) (S \<inter> f -` t)"
   1.847 +  show "openin (top_of_set S) (S \<inter> f -` t)"
   1.848      unfolding * using \<open>open t\<close> assms continuous_openin_preimage_gen openin_trans openin_Union by blast
   1.849  qed
   1.850  
   1.851 @@ -2891,9 +2891,9 @@
   1.852  
   1.853  lemma closedin_union_complement_components:
   1.854    assumes u: "locally connected u"
   1.855 -      and S: "closedin (subtopology euclidean u) S"
   1.856 +      and S: "closedin (top_of_set u) S"
   1.857        and cuS: "c \<subseteq> components(u - S)"
   1.858 -    shows "closedin (subtopology euclidean u) (S \<union> \<Union>c)"
   1.859 +    shows "closedin (top_of_set u) (S \<union> \<Union>c)"
   1.860  proof -
   1.861    have di: "(\<And>S t. S \<in> c \<and> t \<in> c' \<Longrightarrow> disjnt S t) \<Longrightarrow> disjnt (\<Union> c) (\<Union> c')" for c'
   1.862      by (simp add: disjnt_def) blast
   1.863 @@ -2906,13 +2906,13 @@
   1.864      by (metis DiffD1 DiffD2 assms(3) components_nonoverlap disjnt_def subsetCE)
   1.865    ultimately have eq: "S \<union> \<Union>c = u - (\<Union>(components(u - S) - c))"
   1.866      by (auto simp: disjnt_def)
   1.867 -  have *: "openin (subtopology euclidean u) (\<Union>(components (u - S) - c))"
   1.868 +  have *: "openin (top_of_set u) (\<Union>(components (u - S) - c))"
   1.869      apply (rule openin_Union)
   1.870      apply (rule openin_trans [of "u - S"])
   1.871      apply (simp add: u S locally_diff_closed openin_components_locally_connected)
   1.872      apply (simp add: openin_diff S)
   1.873      done
   1.874 -  have "openin (subtopology euclidean u) (u - (u - \<Union>(components (u - S) - c)))"
   1.875 +  have "openin (top_of_set u) (u - (u - \<Union>(components (u - S) - c)))"
   1.876      apply (rule openin_diff, simp)
   1.877      apply (metis closedin_diff closedin_topspace topspace_euclidean_subtopology *)
   1.878      done
   1.879 @@ -2925,7 +2925,7 @@
   1.880    assumes S: "closed S" and c: "c \<subseteq> components(- S)"
   1.881      shows "closed(S \<union> \<Union> c)"
   1.882  proof -
   1.883 -  have "closedin (subtopology euclidean UNIV) (S \<union> \<Union>c)"
   1.884 +  have "closedin (top_of_set UNIV) (S \<union> \<Union>c)"
   1.885      apply (rule closedin_union_complement_components [OF locally_connected_UNIV])
   1.886      using S c apply (simp_all add: Compl_eq_Diff_UNIV)
   1.887      done
   1.888 @@ -2935,11 +2935,11 @@
   1.889  lemma closedin_Un_complement_component:
   1.890    fixes S :: "'a::real_normed_vector set"
   1.891    assumes u: "locally connected u"
   1.892 -      and S: "closedin (subtopology euclidean u) S"
   1.893 +      and S: "closedin (top_of_set u) S"
   1.894        and c: " c \<in> components(u - S)"
   1.895 -    shows "closedin (subtopology euclidean u) (S \<union> c)"
   1.896 +    shows "closedin (top_of_set u) (S \<union> c)"
   1.897  proof -
   1.898 -  have "closedin (subtopology euclidean u) (S \<union> \<Union>{c})"
   1.899 +  have "closedin (top_of_set u) (S \<union> \<Union>{c})"
   1.900      using c by (blast intro: closedin_union_complement_components [OF u S])
   1.901    then show ?thesis
   1.902      by simp
   1.903 @@ -3987,7 +3987,7 @@
   1.904  
   1.905  proposition path_connected_openin_diff_countable:
   1.906    fixes S :: "'a::euclidean_space set"
   1.907 -  assumes "connected S" and ope: "openin (subtopology euclidean (affine hull S)) S"
   1.908 +  assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S"
   1.909        and "\<not> collinear S" "countable T"
   1.910      shows "path_connected(S - T)"
   1.911  proof (clarsimp simp add: path_connected_component)
   1.912 @@ -3995,9 +3995,9 @@
   1.913    assume xy: "x \<in> S" "x \<notin> T" "y \<in> S" "y \<notin> T"
   1.914    show "path_component (S - T) x y"
   1.915    proof (rule connected_equivalence_relation_gen [OF \<open>connected S\<close>, where P = "\<lambda>x. x \<notin> T"])
   1.916 -    show "\<exists>z. z \<in> U \<and> z \<notin> T" if opeU: "openin (subtopology euclidean S) U" and "x \<in> U" for U x
   1.917 +    show "\<exists>z. z \<in> U \<and> z \<notin> T" if opeU: "openin (top_of_set S) U" and "x \<in> U" for U x
   1.918      proof -
   1.919 -      have "openin (subtopology euclidean (affine hull S)) U"
   1.920 +      have "openin (top_of_set (affine hull S)) U"
   1.921          using opeU ope openin_trans by blast
   1.922        with \<open>x \<in> U\<close> obtain r where Usub: "U \<subseteq> affine hull S" and "r > 0"
   1.923                                and subU: "ball x r \<inter> affine hull S \<subseteq> U"
   1.924 @@ -4024,7 +4024,7 @@
   1.925          using \<open>countable T\<close> countable_subset by blast
   1.926        then show ?thesis by blast
   1.927      qed
   1.928 -    show "\<exists>U. openin (subtopology euclidean S) U \<and> x \<in> U \<and>
   1.929 +    show "\<exists>U. openin (top_of_set S) U \<and> x \<in> U \<and>
   1.930                (\<forall>x\<in>U. \<forall>y\<in>U. x \<notin> T \<and> y \<notin> T \<longrightarrow> path_component (S - T) x y)"
   1.931            if "x \<in> S" for x
   1.932      proof -
   1.933 @@ -4046,9 +4046,9 @@
   1.934        proof (intro exI conjI)
   1.935          show "x \<in> ball x r \<inter> affine hull S"
   1.936            using \<open>x \<in> S\<close> \<open>r > 0\<close> by (simp add: hull_inc)
   1.937 -        have "openin (subtopology euclidean (affine hull S)) (ball x r \<inter> affine hull S)"
   1.938 +        have "openin (top_of_set (affine hull S)) (ball x r \<inter> affine hull S)"
   1.939            by (subst inf.commute) (simp add: openin_Int_open)
   1.940 -        then show "openin (subtopology euclidean S) (ball x r \<inter> affine hull S)"
   1.941 +        then show "openin (top_of_set S) (ball x r \<inter> affine hull S)"
   1.942            by (rule openin_subset_trans [OF _ subS Ssub])
   1.943        qed (use * path_component_trans in \<open>auto simp: path_connected_component path_component_of_subset [OF ST]\<close>)
   1.944      qed
   1.945 @@ -4057,7 +4057,7 @@
   1.946  
   1.947  corollary connected_openin_diff_countable:
   1.948    fixes S :: "'a::euclidean_space set"
   1.949 -  assumes "connected S" and ope: "openin (subtopology euclidean (affine hull S)) S"
   1.950 +  assumes "connected S" and ope: "openin (top_of_set (affine hull S)) S"
   1.951        and "\<not> collinear S" "countable T"
   1.952      shows "connected(S - T)"
   1.953    by (metis path_connected_imp_connected path_connected_openin_diff_countable [OF assms])
   1.954 @@ -4074,7 +4074,7 @@
   1.955    case False
   1.956    show ?thesis
   1.957    proof (rule path_connected_openin_diff_countable)
   1.958 -    show "openin (subtopology euclidean (affine hull S)) S"
   1.959 +    show "openin (top_of_set (affine hull S)) S"
   1.960        by (simp add: assms hull_subset open_subset)
   1.961      show "\<not> collinear S"
   1.962        using assms False by (simp add: collinear_aff_dim aff_dim_open)
   1.963 @@ -4329,7 +4329,7 @@
   1.964  
   1.965  proposition%unimportant homeomorphism_moving_point:
   1.966    fixes a :: "'a::euclidean_space"
   1.967 -  assumes ope: "openin (subtopology euclidean (affine hull S)) S"
   1.968 +  assumes ope: "openin (top_of_set (affine hull S)) S"
   1.969        and "S \<subseteq> T"
   1.970        and TS: "T \<subseteq> affine hull S"
   1.971        and S: "connected S" "a \<in> S" "b \<in> S"
   1.972 @@ -4371,7 +4371,7 @@
   1.973      then show "bounded {x. \<not> ((f2 \<circ> f1) x = x \<and> (g1 \<circ> g2) x = x)}"
   1.974        by (rule bounded_subset) auto
   1.975    qed
   1.976 -  have 3: "\<exists>U. openin (subtopology euclidean S) U \<and>
   1.977 +  have 3: "\<exists>U. openin (top_of_set S) U \<and>
   1.978                d \<in> U \<and>
   1.979                (\<forall>x\<in>U.
   1.980                    \<exists>f g. homeomorphism T T f g \<and> f d = x \<and>
   1.981 @@ -4410,7 +4410,7 @@
   1.982    assumes K: "finite K" "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
   1.983               "pairwise (\<lambda>i j. (x i \<noteq> x j) \<and> (y i \<noteq> y j)) K"
   1.984        and "2 \<le> aff_dim S"
   1.985 -      and ope: "openin (subtopology euclidean (affine hull S)) S"
   1.986 +      and ope: "openin (top_of_set (affine hull S)) S"
   1.987        and "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
   1.988    shows "\<exists>f g. homeomorphism T T f g \<and> (\<forall>i \<in> K. f(x i) = y i) \<and>
   1.989                 {x. \<not> (f x = x \<and> g x = x)} \<subseteq> S \<and> bounded {x. \<not> (f x = x \<and> g x = x)}"
   1.990 @@ -4449,7 +4449,7 @@
   1.991                 and hk_sub: "{x. \<not> (h x = x \<and> k x = x)} \<subseteq> S - y ` K"
   1.992                 and bo_hk:  "bounded {x. \<not> (h x = x \<and> k x = x)}"
   1.993    proof (rule homeomorphism_moving_point [of "S - y`K" T "f(x i)" "y i"])
   1.994 -    show "openin (subtopology euclidean (affine hull (S - y ` K))) (S - y ` K)"
   1.995 +    show "openin (top_of_set (affine hull (S - y ` K))) (S - y ` K)"
   1.996        by (simp add: aff_eq openin_diff finite_imp_closedin image_subset_iff hull_inc insert xyS)
   1.997      show "S - y ` K \<subseteq> T"
   1.998        using \<open>S \<subseteq> T\<close> by auto
   1.999 @@ -4499,7 +4499,7 @@
  1.1000    case False
  1.1001    then have affS: "affine hull S = UNIV"
  1.1002      by (simp add: affine_hull_open \<open>open S\<close>)
  1.1003 -  then have ope: "openin (subtopology euclidean (affine hull S)) S"
  1.1004 +  then have ope: "openin (top_of_set (affine hull S)) S"
  1.1005      using \<open>open S\<close> open_openin by auto
  1.1006    have "2 \<le> DIM('a)" by (rule 2)
  1.1007    also have "\<dots> = aff_dim (UNIV :: 'a set)"
  1.1008 @@ -4714,7 +4714,7 @@
  1.1009        using \<open>cbox w z \<subseteq> S\<close> \<open>S \<subseteq> T\<close> by auto
  1.1010      show "homeomorphism T T f' g'"
  1.1011      proof
  1.1012 -      have clo: "closedin (subtopology euclidean (cbox w z \<union> (T - box w z))) (T - box w z)"
  1.1013 +      have clo: "closedin (top_of_set (cbox w z \<union> (T - box w z))) (T - box w z)"
  1.1014          by (metis Diff_Diff_Int Diff_subset T closedin_def open_box openin_open_Int topspace_euclidean_subtopology)
  1.1015        have "continuous_on (cbox w z \<union> (T - box w z)) f'" "continuous_on (cbox w z \<union> (T - box w z)) g'"
  1.1016          unfolding f'_def g'_def
  1.1017 @@ -4830,14 +4830,14 @@
  1.1018  
  1.1019  proposition%unimportant homeomorphism_grouping_points_exists_gen:
  1.1020    fixes S :: "'a::euclidean_space set"
  1.1021 -  assumes opeU: "openin (subtopology euclidean S) U"
  1.1022 -      and opeS: "openin (subtopology euclidean (affine hull S)) S"
  1.1023 +  assumes opeU: "openin (top_of_set S) U"
  1.1024 +      and opeS: "openin (top_of_set (affine hull S)) S"
  1.1025        and "U \<noteq> {}" "finite K" "K \<subseteq> S" and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
  1.1026    obtains f g where "homeomorphism T T f g" "{x. (\<not> (f x = x \<and> g x = x))} \<subseteq> S"
  1.1027                      "bounded {x. (\<not> (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
  1.1028  proof (cases "2 \<le> aff_dim S")
  1.1029    case True
  1.1030 -  have opeU': "openin (subtopology euclidean (affine hull S)) U"
  1.1031 +  have opeU': "openin (top_of_set (affine hull S)) U"
  1.1032      using opeS opeU openin_trans by blast
  1.1033    obtain u where "u \<in> U" "u \<in> S"
  1.1034      using \<open>U \<noteq> {}\<close> opeU openin_imp_subset by fastforce+
  1.1035 @@ -4892,7 +4892,7 @@
  1.1036        by (meson Topological_Spaces.connected_continuous_image \<open>connected S\<close> homeomorphism_cont1 homeomorphism_of_subsets homhj hull_subset top_greatest)
  1.1037      have hUS: "h ` U \<subseteq> h ` S"
  1.1038        by (meson homeomorphism_imp_open_map homeomorphism_of_subsets homhj hull_subset opeS opeU open_UNIV openin_open_eq)
  1.1039 -    have opn: "openin (subtopology euclidean (affine hull S)) U \<Longrightarrow> open (h ` U)" for U
  1.1040 +    have opn: "openin (top_of_set (affine hull S)) U \<Longrightarrow> open (h ` U)" for U
  1.1041        using homeomorphism_imp_open_map [OF homhj]  by simp
  1.1042      have "open (h ` U)" "open (h ` S)"
  1.1043        by (auto intro: opeS opeU openin_trans opn)