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)
```