src/HOL/Analysis/Further_Topology.thy
 changeset 68833 fde093888c16 parent 68634 db0980691ef4 child 69064 5840724b1d71
```     1.1 --- a/src/HOL/Analysis/Further_Topology.thy	Mon Aug 27 22:58:36 2018 +0200
1.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Tue Aug 28 13:28:39 2018 +0100
1.3 @@ -1,4 +1,4 @@
1.4 -section \<open>Extending Continous Maps, Invariance of Domain, etc\<close>
1.5 +section%important \<open>Extending Continous Maps, Invariance of Domain, etc\<close>
1.6
1.7  text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
1.8
1.9 @@ -6,15 +6,15 @@
1.10    imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental
1.11  begin
1.12
1.13 -subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
1.14 -
1.15 -lemma spheremap_lemma1:
1.16 +subsection%important\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
1.17 +
1.18 +lemma%important spheremap_lemma1:
1.19    fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.20    assumes "subspace S" "subspace T" and dimST: "dim S < dim T"
1.21        and "S \<subseteq> T"
1.22        and diff_f: "f differentiable_on sphere 0 1 \<inter> S"
1.23      shows "f ` (sphere 0 1 \<inter> S) \<noteq> sphere 0 1 \<inter> T"
1.24 -proof
1.25 +proof%unimportant
1.26    assume fim: "f ` (sphere 0 1 \<inter> S) = sphere 0 1 \<inter> T"
1.27    have inS: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x /\<^sub>R norm x) \<in> S"
1.28      using subspace_mul \<open>subspace S\<close> by blast
1.29 @@ -158,14 +158,14 @@
1.30  qed
1.31
1.32
1.33 -lemma spheremap_lemma2:
1.34 +lemma%important spheremap_lemma2:
1.35    fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.36    assumes ST: "subspace S" "subspace T" "dim S < dim T"
1.37        and "S \<subseteq> T"
1.38        and contf: "continuous_on (sphere 0 1 \<inter> S) f"
1.39        and fim: "f ` (sphere 0 1 \<inter> S) \<subseteq> sphere 0 1 \<inter> T"
1.40      shows "\<exists>c. homotopic_with (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)"
1.41 -proof -
1.42 +proof%unimportant -
1.43    have [simp]: "\<And>x. \<lbrakk>norm x = 1; x \<in> S\<rbrakk> \<Longrightarrow> norm (f x) = 1"
1.44      using fim by (simp add: image_subset_iff)
1.45    have "compact (sphere 0 1 \<inter> S)"
1.46 @@ -252,11 +252,11 @@
1.47  qed
1.48
1.49
1.50 -lemma spheremap_lemma3:
1.51 +lemma%important spheremap_lemma3:
1.52    assumes "bounded S" "convex S" "subspace U" and affSU: "aff_dim S \<le> dim U"
1.53    obtains T where "subspace T" "T \<subseteq> U" "S \<noteq> {} \<Longrightarrow> aff_dim T = aff_dim S"
1.54                    "(rel_frontier S) homeomorphic (sphere 0 1 \<inter> T)"
1.55 -proof (cases "S = {}")
1.56 +proof%unimportant (cases "S = {}")
1.57    case True
1.58    with \<open>subspace U\<close> subspace_0 show ?thesis
1.59      by (rule_tac T = "{0}" in that) auto
1.60 @@ -300,14 +300,14 @@
1.61  qed
1.62
1.63
1.64 -proposition inessential_spheremap_lowdim_gen:
1.65 +proposition%important inessential_spheremap_lowdim_gen:
1.66    fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.67    assumes "convex S" "bounded S" "convex T" "bounded T"
1.68        and affST: "aff_dim S < aff_dim T"
1.69        and contf: "continuous_on (rel_frontier S) f"
1.70        and fim: "f ` (rel_frontier S) \<subseteq> rel_frontier T"
1.71    obtains c where "homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
1.72 -proof (cases "S = {}")
1.73 +proof%unimportant (cases "S = {}")
1.74    case True
1.75    then show ?thesis
1.77 @@ -350,7 +350,7 @@
1.78    qed
1.79  qed
1.80
1.81 -lemma inessential_spheremap_lowdim:
1.82 +lemma%unimportant inessential_spheremap_lowdim:
1.83    fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space"
1.84    assumes
1.85     "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \<subseteq> (sphere b s)"
1.86 @@ -377,9 +377,9 @@
1.87
1.88
1.89
1.90 -subsection\<open> Some technical lemmas about extending maps from cell complexes\<close>
1.91 -
1.92 -lemma extending_maps_Union_aux:
1.93 +subsection%important\<open> Some technical lemmas about extending maps from cell complexes\<close>
1.94 +
1.95 +lemma%unimportant extending_maps_Union_aux:
1.96    assumes fin: "finite \<F>"
1.97        and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
1.98        and "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>; S \<noteq> T\<rbrakk> \<Longrightarrow> S \<inter> T \<subseteq> K"
1.99 @@ -410,7 +410,7 @@
1.100      done
1.101  qed
1.102
1.103 -lemma extending_maps_Union:
1.104 +lemma%unimportant extending_maps_Union:
1.105    assumes fin: "finite \<F>"
1.106        and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
1.107        and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
1.108 @@ -422,14 +422,14 @@
1.109  by (metis K psubsetI)
1.110
1.111
1.112 -lemma extend_map_lemma:
1.113 +lemma%important extend_map_lemma:
1.114    assumes "finite \<F>" "\<G> \<subseteq> \<F>" "convex T" "bounded T"
1.115        and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
1.116        and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X < aff_dim T"
1.117        and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T"
1.118        and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
1.119    obtains g where "continuous_on (\<Union>\<F>) g" "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
1.120 -proof (cases "\<F> - \<G> = {}")
1.121 +proof%unimportant (cases "\<F> - \<G> = {}")
1.122    case True
1.123    then have "\<Union>\<F> \<subseteq> \<Union>\<G>"
1.125 @@ -608,7 +608,7 @@
1.126      using extendf [of i] unfolding eq by (metis that)
1.127  qed
1.128
1.129 -lemma extend_map_lemma_cofinite0:
1.130 +lemma%unimportant extend_map_lemma_cofinite0:
1.131    assumes "finite \<F>"
1.132        and "pairwise (\<lambda>S T. S \<inter> T \<subseteq> K) \<F>"
1.133        and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g ` (S - {a}) \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
1.134 @@ -665,7 +665,7 @@
1.135  qed
1.136
1.137
1.138 -lemma extend_map_lemma_cofinite1:
1.139 +lemma%unimportant extend_map_lemma_cofinite1:
1.140  assumes "finite \<F>"
1.141      and \<F>: "\<And>X. X \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (X - {a}) g \<and> g ` (X - {a}) \<subseteq> T \<and> (\<forall>x \<in> X \<inter> K. g x = h x)"
1.142      and clo: "\<And>X. X \<in> \<F> \<Longrightarrow> closed X"
1.143 @@ -695,7 +695,7 @@
1.144  qed
1.145
1.146
1.147 -lemma extend_map_lemma_cofinite:
1.148 +lemma%important extend_map_lemma_cofinite:
1.149    assumes "finite \<F>" "\<G> \<subseteq> \<F>" and T: "convex T" "bounded T"
1.150        and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
1.151        and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
1.152 @@ -704,7 +704,7 @@
1.153    obtains C g where
1.154       "finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
1.155       "g ` (\<Union> \<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
1.156 -proof -
1.157 +proof%unimportant -
1.158    define \<H> where "\<H> \<equiv> \<G> \<union> {D. \<exists>C \<in> \<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}"
1.159    have "finite \<G>"
1.160      using assms finite_subset by blast
1.161 @@ -869,7 +869,7 @@
1.162  qed
1.163
1.164  text\<open>The next two proofs are similar\<close>
1.165 -theorem extend_map_cell_complex_to_sphere:
1.166 +theorem%important extend_map_cell_complex_to_sphere:
1.167    assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T"
1.168        and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
1.169        and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X < aff_dim T"
1.170 @@ -877,7 +877,7 @@
1.171        and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
1.172    obtains g where "continuous_on (\<Union>\<F>) g"
1.173       "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.174 -proof -
1.175 +proof%unimportant -
1.176    obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g ` V \<subseteq> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.177      using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
1.178    have "compact S"
1.179 @@ -924,7 +924,7 @@
1.180  qed
1.181
1.182
1.183 -theorem extend_map_cell_complex_to_sphere_cofinite:
1.184 +theorem%important extend_map_cell_complex_to_sphere_cofinite:
1.185    assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T"
1.186        and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
1.187        and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> aff_dim T"
1.188 @@ -932,7 +932,7 @@
1.189        and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
1.190    obtains C g where "finite C" "disjnt C S" "continuous_on (\<Union>\<F> - C) g"
1.191       "g ` (\<Union>\<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.192 -proof -
1.193 +proof%unimportant -
1.194    obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g ` V \<subseteq> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.195      using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
1.196    have "compact S"
1.197 @@ -991,12 +991,12 @@
1.198
1.199
1.200
1.201 -subsection\<open> Special cases and corollaries involving spheres\<close>
1.202 -
1.203 -lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
1.204 +subsection%important\<open> Special cases and corollaries involving spheres\<close>
1.205 +
1.206 +lemma%unimportant disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
1.207    by (auto simp: disjnt_def)
1.208
1.209 -proposition extend_map_affine_to_sphere_cofinite_simple:
1.210 +proposition%important extend_map_affine_to_sphere_cofinite_simple:
1.211    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.212    assumes "compact S" "convex U" "bounded U"
1.213        and aff: "aff_dim T \<le> aff_dim U"
1.214 @@ -1005,7 +1005,7 @@
1.215   obtains K g where "finite K" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
1.216                     "g ` (T - K) \<subseteq> rel_frontier U"
1.217                     "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.218 -proof -
1.219 +proof%unimportant -
1.220    have "\<exists>K g. finite K \<and> disjnt K S \<and> continuous_on (T - K) g \<and>
1.221                g ` (T - K) \<subseteq> rel_frontier U \<and> (\<forall>x \<in> S. g x = f x)"
1.222         if "affine T" "S \<subseteq> T" and aff: "aff_dim T \<le> aff_dim U"  for T
1.223 @@ -1140,18 +1140,18 @@
1.224      by (rule_tac K="K \<inter> T" and g=g in that) (auto simp: disjnt_iff Diff_Int contg)
1.225  qed
1.226
1.227 -subsection\<open>Extending maps to spheres\<close>
1.228 +subsection%important\<open>Extending maps to spheres\<close>
1.229
1.230  (*Up to extend_map_affine_to_sphere_cofinite_gen*)
1.231
1.232 -lemma extend_map_affine_to_sphere1:
1.233 +lemma%important extend_map_affine_to_sphere1:
1.234    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::topological_space"
1.235    assumes "finite K" "affine U" and contf: "continuous_on (U - K) f"
1.236        and fim: "f ` (U - K) \<subseteq> T"
1.237        and comps: "\<And>C. \<lbrakk>C \<in> components(U - S); C \<inter> K \<noteq> {}\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
1.238        and clo: "closedin (subtopology euclidean U) S" and K: "disjnt K S" "K \<subseteq> U"
1.239    obtains g where "continuous_on (U - L) g" "g ` (U - L) \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.240 -proof (cases "K = {}")
1.241 +proof%unimportant (cases "K = {}")
1.242    case True
1.243    then show ?thesis
1.244      by (metis Diff_empty Diff_subset contf fim continuous_on_subset image_subsetI rev_image_eqI subset_iff that)
1.245 @@ -1436,7 +1436,7 @@
1.246  qed
1.247
1.248
1.249 -lemma extend_map_affine_to_sphere2:
1.250 +lemma%important extend_map_affine_to_sphere2:
1.251    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.252    assumes "compact S" "convex U" "bounded U" "affine T" "S \<subseteq> T"
1.253        and affTU: "aff_dim T \<le> aff_dim U"
1.254 @@ -1446,7 +1446,7 @@
1.255      obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S"
1.256                        "continuous_on (T - K) g" "g ` (T - K) \<subseteq> rel_frontier U"
1.257                        "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.258 -proof -
1.259 +proof%unimportant -
1.260    obtain K g where K: "finite K" "K \<subseteq> T" "disjnt K S"
1.261                 and contg: "continuous_on (T - K) g"
1.262                 and gim: "g ` (T - K) \<subseteq> rel_frontier U"
1.263 @@ -1490,7 +1490,7 @@
1.264  qed
1.265
1.266
1.267 -proposition extend_map_affine_to_sphere_cofinite_gen:
1.268 +proposition%important extend_map_affine_to_sphere_cofinite_gen:
1.269    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.270    assumes SUT: "compact S" "convex U" "bounded U" "affine T" "S \<subseteq> T"
1.271        and aff: "aff_dim T \<le> aff_dim U"
1.272 @@ -1500,7 +1500,7 @@
1.273   obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
1.274                     "g ` (T - K) \<subseteq> rel_frontier U"
1.275                     "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.276 -proof (cases "S = {}")
1.277 +proof%unimportant (cases "S = {}")
1.278    case True
1.279    show ?thesis
1.280    proof (cases "rel_frontier U = {}")
1.281 @@ -1645,7 +1645,7 @@
1.282  qed
1.283
1.284
1.285 -corollary extend_map_affine_to_sphere_cofinite:
1.286 +corollary%important extend_map_affine_to_sphere_cofinite:
1.287    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.288    assumes SUT: "compact S" "affine T" "S \<subseteq> T"
1.289        and aff: "aff_dim T \<le> DIM('b)" and "0 \<le> r"
1.290 @@ -1654,7 +1654,7 @@
1.291        and dis: "\<And>C. \<lbrakk>C \<in> components(T - S); bounded C\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
1.292    obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
1.293                      "g ` (T - K) \<subseteq> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.294 -proof (cases "r = 0")
1.295 +proof%unimportant (cases "r = 0")
1.296    case True
1.297    with fim show ?thesis
1.298      by (rule_tac K="{}" and g = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
1.299 @@ -1670,7 +1670,7 @@
1.300      done
1.301  qed
1.302
1.303 -corollary extend_map_UNIV_to_sphere_cofinite:
1.304 +corollary%important extend_map_UNIV_to_sphere_cofinite:
1.305    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.306    assumes aff: "DIM('a) \<le> DIM('b)" and "0 \<le> r"
1.307        and SUT: "compact S"
1.308 @@ -1684,7 +1684,7 @@
1.309   apply (auto simp: assms that Compl_eq_Diff_UNIV [symmetric])
1.310  done
1.311
1.312 -corollary extend_map_UNIV_to_sphere_no_bounded_component:
1.313 +corollary%important extend_map_UNIV_to_sphere_no_bounded_component:
1.314    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.315    assumes aff: "DIM('a) \<le> DIM('b)" and "0 \<le> r"
1.316        and SUT: "compact S"
1.317 @@ -1696,14 +1696,14 @@
1.318     apply (auto simp: that dest: dis)
1.319  done
1.320
1.321 -theorem Borsuk_separation_theorem_gen:
1.322 +theorem%important Borsuk_separation_theorem_gen:
1.323    fixes S :: "'a::euclidean_space set"
1.324    assumes "compact S"
1.325      shows "(\<forall>c \<in> components(- S). ~bounded c) \<longleftrightarrow>
1.326             (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
1.327                  \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
1.328         (is "?lhs = ?rhs")
1.329 -proof
1.330 +proof%unimportant
1.331    assume L [rule_format]: ?lhs
1.332    show ?rhs
1.333    proof clarify
1.334 @@ -1734,14 +1734,14 @@
1.335  qed
1.336
1.337
1.338 -corollary Borsuk_separation_theorem:
1.339 +corollary%important Borsuk_separation_theorem:
1.340    fixes S :: "'a::euclidean_space set"
1.341    assumes "compact S" and 2: "2 \<le> DIM('a)"
1.342      shows "connected(- S) \<longleftrightarrow>
1.343             (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
1.344                  \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
1.345         (is "?lhs = ?rhs")
1.346 -proof
1.347 +proof%unimportant
1.348    assume L: ?lhs
1.349    show ?rhs
1.350    proof (cases "S = {}")
1.351 @@ -1764,7 +1764,7 @@
1.352  qed
1.353
1.354
1.355 -lemma homotopy_eqv_separation:
1.356 +lemma%unimportant homotopy_eqv_separation:
1.357    fixes S :: "'a::euclidean_space set" and T :: "'a set"
1.358    assumes "S homotopy_eqv T" and "compact S" and "compact T"
1.359    shows "connected(- S) \<longleftrightarrow> connected(- T)"
1.360 @@ -1783,11 +1783,11 @@
1.361    qed
1.362  qed
1.363
1.364 -lemma Jordan_Brouwer_separation:
1.365 +lemma%important Jordan_Brouwer_separation:
1.366    fixes S :: "'a::euclidean_space set" and a::'a
1.367    assumes hom: "S homeomorphic sphere a r" and "0 < r"
1.368      shows "\<not> connected(- S)"
1.369 -proof -
1.370 +proof%unimportant -
1.371    have "- sphere a r \<inter> ball a r \<noteq> {}"
1.372      using \<open>0 < r\<close> by (simp add: Int_absorb1 subset_eq)
1.373    moreover
1.374 @@ -1817,11 +1817,11 @@
1.375  qed
1.376
1.377
1.378 -lemma Jordan_Brouwer_frontier:
1.379 +lemma%important Jordan_Brouwer_frontier:
1.380    fixes S :: "'a::euclidean_space set" and a::'a
1.381    assumes S: "S homeomorphic sphere a r" and T: "T \<in> components(- S)" and 2: "2 \<le> DIM('a)"
1.382      shows "frontier T = S"
1.383 -proof (cases r rule: linorder_cases)
1.384 +proof%unimportant (cases r rule: linorder_cases)
1.385    assume "r < 0"
1.386    with S T show ?thesis by auto
1.387  next
1.388 @@ -1866,11 +1866,11 @@
1.389    qed (rule T)
1.390  qed
1.391
1.392 -lemma Jordan_Brouwer_nonseparation:
1.393 +lemma%important Jordan_Brouwer_nonseparation:
1.394    fixes S :: "'a::euclidean_space set" and a::'a
1.395    assumes S: "S homeomorphic sphere a r" and "T \<subset> S" and 2: "2 \<le> DIM('a)"
1.396      shows "connected(- T)"
1.397 -proof -
1.398 +proof%unimportant -
1.399    have *: "connected(C \<union> (S - T))" if "C \<in> components(- S)" for C
1.400    proof (rule connected_intermediate_closure)
1.401      show "connected C"
1.402 @@ -1892,9 +1892,9 @@
1.403      done
1.404  qed
1.405
1.406 -subsection\<open> Invariance of domain and corollaries\<close>
1.407 -
1.408 -lemma invariance_of_domain_ball:
1.409 +subsection%important\<open> Invariance of domain and corollaries\<close>
1.410 +
1.411 +lemma%unimportant invariance_of_domain_ball:
1.412    fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
1.413    assumes contf: "continuous_on (cball a r) f" and "0 < r"
1.414       and inj: "inj_on f (cball a r)"
1.415 @@ -1982,12 +1982,12 @@
1.416
1.417
1.418  text\<open>Proved by L. E. J. Brouwer (1912)\<close>
1.419 -theorem invariance_of_domain:
1.420 +theorem%important invariance_of_domain:
1.421    fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
1.422    assumes "continuous_on S f" "open S" "inj_on f S"
1.423      shows "open(f ` S)"
1.424    unfolding open_subopen [of "f`S"]
1.425 -proof clarify
1.426 +proof%unimportant clarify
1.427    fix a
1.428    assume "a \<in> S"
1.429    obtain \<delta> where "\<delta> > 0" and \<delta>: "cball a \<delta> \<subseteq> S"
1.430 @@ -2003,7 +2003,7 @@
1.431    qed
1.432  qed
1.433
1.434 -lemma inv_of_domain_ss0:
1.435 +lemma%unimportant inv_of_domain_ss0:
1.436    fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
1.437    assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
1.438        and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)"
1.439 @@ -2049,7 +2049,7 @@
1.440      by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
1.441  qed
1.442
1.443 -lemma inv_of_domain_ss1:
1.444 +lemma%unimportant inv_of_domain_ss1:
1.445    fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
1.446    assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
1.447        and "subspace S"
1.448 @@ -2090,14 +2090,14 @@
1.449  qed
1.450
1.451
1.452 -corollary invariance_of_domain_subspaces:
1.453 +corollary%important invariance_of_domain_subspaces:
1.454    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.455    assumes ope: "openin (subtopology euclidean U) S"
1.456        and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
1.457        and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
1.458        and injf: "inj_on f S"
1.459      shows "openin (subtopology euclidean V) (f ` S)"
1.460 -proof -
1.461 +proof%unimportant -
1.462    obtain V' where "subspace V'" "V' \<subseteq> U" "dim V' = dim V"
1.463      using choose_subspace_of_subspace [OF VU]
1.464      by (metis span_eq_iff \<open>subspace U\<close>)
1.465 @@ -2134,14 +2134,14 @@
1.466    qed
1.467  qed
1.468
1.469 -corollary invariance_of_dimension_subspaces:
1.470 +corollary%important invariance_of_dimension_subspaces:
1.471    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.472    assumes ope: "openin (subtopology euclidean U) S"
1.473        and "subspace U" "subspace V"
1.474        and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
1.475        and injf: "inj_on f S" and "S \<noteq> {}"
1.476      shows "dim U \<le> dim V"
1.477 -proof -
1.478 +proof%unimportant -
1.479    have "False" if "dim V < dim U"
1.480    proof -
1.481      obtain T where "subspace T" "T \<subseteq> U" "dim T = dim V"
1.482 @@ -2169,14 +2169,14 @@
1.483      using not_less by blast
1.484  qed
1.485
1.486 -corollary invariance_of_domain_affine_sets:
1.487 +corollary%important invariance_of_domain_affine_sets:
1.488    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.489    assumes ope: "openin (subtopology euclidean U) S"
1.490        and aff: "affine U" "affine V" "aff_dim V \<le> aff_dim U"
1.491        and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
1.492        and injf: "inj_on f S"
1.493      shows "openin (subtopology euclidean V) (f ` S)"
1.494 -proof (cases "S = {}")
1.495 +proof%unimportant (cases "S = {}")
1.496    case True
1.497    then show ?thesis by auto
1.498  next
1.499 @@ -2204,14 +2204,14 @@
1.500      by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois)
1.501  qed
1.502
1.503 -corollary invariance_of_dimension_affine_sets:
1.504 +corollary%important invariance_of_dimension_affine_sets:
1.505    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.506    assumes ope: "openin (subtopology euclidean U) S"
1.507        and aff: "affine U" "affine V"
1.508        and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
1.509        and injf: "inj_on f S" and "S \<noteq> {}"
1.510      shows "aff_dim U \<le> aff_dim V"
1.511 -proof -
1.512 +proof%unimportant -
1.513    obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
1.514      using \<open>S \<noteq> {}\<close> fim ope openin_contains_cball by fastforce
1.515    have "dim ((+) (- a) ` U) \<le> dim ((+) (- b) ` V)"
1.516 @@ -2233,25 +2233,25 @@
1.517      by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
1.518  qed
1.519
1.520 -corollary invariance_of_dimension:
1.521 +corollary%important invariance_of_dimension:
1.522    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.523    assumes contf: "continuous_on S f" and "open S"
1.524        and injf: "inj_on f S" and "S \<noteq> {}"
1.525      shows "DIM('a) \<le> DIM('b)"
1.526 -  using invariance_of_dimension_subspaces [of UNIV S UNIV f] assms
1.527 +  using%unimportant invariance_of_dimension_subspaces [of UNIV S UNIV f] assms
1.528    by auto
1.529
1.530
1.531 -corollary continuous_injective_image_subspace_dim_le:
1.532 +corollary%important continuous_injective_image_subspace_dim_le:
1.533    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.534    assumes "subspace S" "subspace T"
1.535        and contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
1.536        and injf: "inj_on f S"
1.537      shows "dim S \<le> dim T"
1.538    apply (rule invariance_of_dimension_subspaces [of S S _ f])
1.539 -  using assms by (auto simp: subspace_affine)
1.540 -
1.541 -lemma invariance_of_dimension_convex_domain:
1.542 +  using%unimportant assms by (auto simp: subspace_affine)
1.543 +
1.544 +lemma%unimportant invariance_of_dimension_convex_domain:
1.545    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.546    assumes "convex S"
1.547        and contf: "continuous_on S f" and fim: "f ` S \<subseteq> affine hull T"
1.548 @@ -2280,7 +2280,7 @@
1.549  qed
1.550
1.551
1.552 -lemma homeomorphic_convex_sets_le:
1.553 +lemma%unimportant homeomorphic_convex_sets_le:
1.554    assumes "convex S" "S homeomorphic T"
1.555    shows "aff_dim S \<le> aff_dim T"
1.556  proof -
1.557 @@ -2297,23 +2297,23 @@
1.558    qed
1.559  qed
1.560
1.561 -lemma homeomorphic_convex_sets:
1.562 +lemma%unimportant homeomorphic_convex_sets:
1.563    assumes "convex S" "convex T" "S homeomorphic T"
1.564    shows "aff_dim S = aff_dim T"
1.565    by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym)
1.566
1.567 -lemma homeomorphic_convex_compact_sets_eq:
1.568 +lemma%unimportant homeomorphic_convex_compact_sets_eq:
1.569    assumes "convex S" "compact S" "convex T" "compact T"
1.570    shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
1.571    by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets)
1.572
1.573 -lemma invariance_of_domain_gen:
1.574 +lemma%unimportant invariance_of_domain_gen:
1.575    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.576    assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
1.577      shows "open(f ` S)"
1.578    using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto
1.579
1.580 -lemma injective_into_1d_imp_open_map_UNIV:
1.581 +lemma%unimportant injective_into_1d_imp_open_map_UNIV:
1.582    fixes f :: "'a::euclidean_space \<Rightarrow> real"
1.583    assumes "open T" "continuous_on S f" "inj_on f S" "T \<subseteq> S"
1.584      shows "open (f ` T)"
1.585 @@ -2321,7 +2321,7 @@
1.586    using assms apply (auto simp: elim: continuous_on_subset subset_inj_on)
1.587    done
1.588
1.589 -lemma continuous_on_inverse_open:
1.590 +lemma%unimportant continuous_on_inverse_open:
1.591    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.592    assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" and gf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
1.593      shows "continuous_on (f ` S) g"
1.594 @@ -2340,7 +2340,7 @@
1.595      by (metis \<open>open T\<close> continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq)
1.596  qed
1.597
1.598 -lemma invariance_of_domain_homeomorphism:
1.599 +lemma%unimportant invariance_of_domain_homeomorphism:
1.600    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.601    assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
1.602    obtains g where "homeomorphism S (f ` S) f g"
1.603 @@ -2349,14 +2349,14 @@
1.604      by (simp add: assms continuous_on_inverse_open homeomorphism_def)
1.605  qed
1.606
1.607 -corollary invariance_of_domain_homeomorphic:
1.608 +corollary%important invariance_of_domain_homeomorphic:
1.609    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.610    assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
1.611    shows "S homeomorphic (f ` S)"
1.612 -  using invariance_of_domain_homeomorphism [OF assms]
1.613 -  by (meson homeomorphic_def)
1.614 -
1.615 -lemma continuous_image_subset_interior:
1.616 +  using%unimportant invariance_of_domain_homeomorphism [OF assms]
1.617 +  by%unimportant (meson homeomorphic_def)
1.618 +
1.619 +lemma%unimportant continuous_image_subset_interior:
1.620    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.621    assumes "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
1.622    shows "f ` (interior S) \<subseteq> interior(f ` S)"
1.623 @@ -2367,13 +2367,13 @@
1.624       apply (auto simp: subset_inj_on interior_subset continuous_on_subset)
1.625    done
1.626
1.627 -lemma homeomorphic_interiors_same_dimension:
1.628 +lemma%important homeomorphic_interiors_same_dimension:
1.629    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.630    assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)"
1.631    shows "(interior S) homeomorphic (interior T)"
1.632    using assms [unfolded homeomorphic_minimal]
1.633    unfolding homeomorphic_def
1.634 -proof (clarify elim!: ex_forward)
1.635 +proof%unimportant (clarify elim!: ex_forward)
1.636    fix f g
1.637    assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
1.638       and contf: "continuous_on S f" and contg: "continuous_on T g"
1.639 @@ -2417,7 +2417,7 @@
1.640    qed
1.641  qed
1.642
1.643 -lemma homeomorphic_open_imp_same_dimension:
1.644 +lemma%unimportant homeomorphic_open_imp_same_dimension:
1.645    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.646    assumes "S homeomorphic T" "open S" "S \<noteq> {}" "open T" "T \<noteq> {}"
1.647    shows "DIM('a) = DIM('b)"
1.648 @@ -2426,7 +2426,7 @@
1.649      apply (rule order_antisym; metis inj_onI invariance_of_dimension)
1.650      done
1.651
1.652 -lemma homeomorphic_interiors:
1.653 +lemma%unimportant homeomorphic_interiors:
1.654    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.655    assumes "S homeomorphic T" "interior S = {} \<longleftrightarrow> interior T = {}"
1.656      shows "(interior S) homeomorphic (interior T)"
1.657 @@ -2444,7 +2444,7 @@
1.658      by (rule homeomorphic_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
1.659  qed
1.660
1.661 -lemma homeomorphic_frontiers_same_dimension:
1.662 +lemma%unimportant homeomorphic_frontiers_same_dimension:
1.663    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.664    assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)"
1.665    shows "(frontier S) homeomorphic (frontier T)"
1.666 @@ -2500,7 +2500,7 @@
1.667    qed
1.668  qed
1.669
1.670 -lemma homeomorphic_frontiers:
1.671 +lemma%unimportant homeomorphic_frontiers:
1.672    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.673    assumes "S homeomorphic T" "closed S" "closed T"
1.674            "interior S = {} \<longleftrightarrow> interior T = {}"
1.675 @@ -2517,7 +2517,7 @@
1.676      using False assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast
1.677  qed
1.678
1.679 -lemma continuous_image_subset_rel_interior:
1.680 +lemma%unimportant continuous_image_subset_rel_interior:
1.681    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.682    assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
1.683        and TS: "aff_dim T \<le> aff_dim S"
1.684 @@ -2540,7 +2540,7 @@
1.685    qed auto
1.686  qed
1.687
1.688 -lemma homeomorphic_rel_interiors_same_dimension:
1.689 +lemma%unimportant homeomorphic_rel_interiors_same_dimension:
1.690    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.691    assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
1.692    shows "(rel_interior S) homeomorphic (rel_interior T)"
1.693 @@ -2592,11 +2592,11 @@
1.694    qed
1.695  qed
1.696
1.697 -lemma homeomorphic_rel_interiors:
1.698 +lemma%important homeomorphic_rel_interiors:
1.699    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.700    assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
1.701      shows "(rel_interior S) homeomorphic (rel_interior T)"
1.702 -proof (cases "rel_interior T = {}")
1.703 +proof%unimportant (cases "rel_interior T = {}")
1.704    case True
1.705    with assms show ?thesis by auto
1.706  next
1.707 @@ -2625,7 +2625,7 @@
1.708  qed
1.709
1.710
1.711 -lemma homeomorphic_rel_boundaries_same_dimension:
1.712 +lemma%unimportant homeomorphic_rel_boundaries_same_dimension:
1.713    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.714    assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
1.715    shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
1.716 @@ -2659,7 +2659,7 @@
1.717    qed
1.718  qed
1.719
1.720 -lemma homeomorphic_rel_boundaries:
1.721 +lemma%unimportant homeomorphic_rel_boundaries:
1.722    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.723    assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
1.724      shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
1.725 @@ -2691,11 +2691,11 @@
1.726      by (rule homeomorphic_rel_boundaries_same_dimension [OF \<open>S homeomorphic T\<close>])
1.727  qed
1.728
1.729 -proposition uniformly_continuous_homeomorphism_UNIV_trivial:
1.730 +proposition%important uniformly_continuous_homeomorphism_UNIV_trivial:
1.731    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
1.732    assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g"
1.733    shows "S = UNIV"
1.734 -proof (cases "S = {}")
1.735 +proof%unimportant (cases "S = {}")
1.736    case True
1.737    then show ?thesis
1.738      by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI)
1.739 @@ -2737,9 +2737,9 @@
1.740      using clopen [of S] False  by simp
1.741  qed
1.742
1.743 -subsection\<open>Dimension-based conditions for various homeomorphisms\<close>
1.744 -
1.745 -lemma homeomorphic_subspaces_eq:
1.746 +subsection%important\<open>Dimension-based conditions for various homeomorphisms\<close>
1.747 +
1.748 +lemma%unimportant homeomorphic_subspaces_eq:
1.749    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.750    assumes "subspace S" "subspace T"
1.751    shows "S homeomorphic T \<longleftrightarrow> dim S = dim T"
1.752 @@ -2760,7 +2760,7 @@
1.753      by (simp add: assms homeomorphic_subspaces)
1.754  qed
1.755
1.756 -lemma homeomorphic_affine_sets_eq:
1.757 +lemma%unimportant homeomorphic_affine_sets_eq:
1.758    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.759    assumes "affine S" "affine T"
1.760    shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
1.761 @@ -2778,19 +2778,19 @@
1.762      by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
1.763  qed
1.764
1.765 -lemma homeomorphic_hyperplanes_eq:
1.766 +lemma%unimportant homeomorphic_hyperplanes_eq:
1.767    fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space"
1.768    assumes "a \<noteq> 0" "c \<noteq> 0"
1.769    shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('a) = DIM('b))"
1.770    apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms)
1.771    by (metis DIM_positive Suc_pred)
1.772
1.773 -lemma homeomorphic_UNIV_UNIV:
1.774 +lemma%unimportant homeomorphic_UNIV_UNIV:
1.775    shows "(UNIV::'a set) homeomorphic (UNIV::'b set) \<longleftrightarrow>
1.776      DIM('a::euclidean_space) = DIM('b::euclidean_space)"
1.778
1.779 -lemma simply_connected_sphere_gen:
1.780 +lemma%unimportant simply_connected_sphere_gen:
1.781     assumes "convex S" "bounded S" and 3: "3 \<le> aff_dim S"
1.782     shows "simply_connected(rel_frontier S)"
1.783  proof -
1.784 @@ -2814,16 +2814,16 @@
1.785    qed
1.786  qed
1.787
1.788 -subsection\<open>more invariance of domain\<close>
1.789 -
1.790 -proposition invariance_of_domain_sphere_affine_set_gen:
1.791 +subsection%important\<open>more invariance of domain\<close>
1.792 +
1.793 +proposition%important invariance_of_domain_sphere_affine_set_gen:
1.794    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.795    assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
1.796        and U: "bounded U" "convex U"
1.797        and "affine T" and affTU: "aff_dim T < aff_dim U"
1.798        and ope: "openin (subtopology euclidean (rel_frontier U)) S"
1.799     shows "openin (subtopology euclidean T) (f ` S)"
1.800 -proof (cases "rel_frontier U = {}")
1.801 +proof%unimportant (cases "rel_frontier U = {}")
1.802    case True
1.803    then show ?thesis
1.804      using ope openin_subset by force
1.805 @@ -2922,7 +2922,7 @@
1.806  qed
1.807
1.808
1.809 -lemma invariance_of_domain_sphere_affine_set:
1.810 +lemma%unimportant invariance_of_domain_sphere_affine_set:
1.811    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.812    assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
1.813        and "r \<noteq> 0" "affine T" and affTU: "aff_dim T < DIM('a)"
1.814 @@ -2943,7 +2943,7 @@
1.815    qed
1.816  qed
1.817
1.818 -lemma no_embedding_sphere_lowdim:
1.819 +lemma%unimportant no_embedding_sphere_lowdim:
1.820    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.821    assumes contf: "continuous_on (sphere a r) f" and injf: "inj_on f (sphere a r)" and "r > 0"
1.822     shows "DIM('a) \<le> DIM('b)"
1.823 @@ -2964,7 +2964,7 @@
1.824      using not_less by blast
1.825  qed
1.826
1.827 -lemma simply_connected_sphere:
1.828 +lemma%unimportant simply_connected_sphere:
1.829    fixes a :: "'a::euclidean_space"
1.830    assumes "3 \<le> DIM('a)"
1.831      shows "simply_connected(sphere a r)"
1.832 @@ -2981,7 +2981,7 @@
1.834  qed
1.835
1.836 -lemma simply_connected_sphere_eq:
1.837 +lemma%unimportant simply_connected_sphere_eq:
1.838    fixes a :: "'a::euclidean_space"
1.839    shows "simply_connected(sphere a r) \<longleftrightarrow> 3 \<le> DIM('a) \<or> r \<le> 0"  (is "?lhs = ?rhs")
1.840  proof (cases "r \<le> 0")
1.841 @@ -3024,7 +3024,7 @@
1.842  qed
1.843
1.844
1.845 -lemma simply_connected_punctured_universe_eq:
1.846 +lemma%unimportant simply_connected_punctured_universe_eq:
1.847    fixes a :: "'a::euclidean_space"
1.848    shows "simply_connected(- {a}) \<longleftrightarrow> 3 \<le> DIM('a)"
1.849  proof -
1.850 @@ -3042,17 +3042,17 @@
1.851    finally show ?thesis .
1.852  qed
1.853
1.854 -lemma not_simply_connected_circle:
1.855 +lemma%unimportant not_simply_connected_circle:
1.856    fixes a :: complex
1.857    shows "0 < r \<Longrightarrow> \<not> simply_connected(sphere a r)"
1.859
1.860
1.861 -proposition simply_connected_punctured_convex:
1.862 +proposition%important simply_connected_punctured_convex:
1.863    fixes a :: "'a::euclidean_space"
1.864    assumes "convex S" and 3: "3 \<le> aff_dim S"
1.865      shows "simply_connected(S - {a})"
1.866 -proof (cases "a \<in> rel_interior S")
1.867 +proof%unimportant (cases "a \<in> rel_interior S")
1.868    case True
1.869    then obtain e where "a \<in> S" "0 < e" and e: "cball a e \<inter> affine hull S \<subseteq> S"
1.870      by (auto simp: rel_interior_cball)
1.871 @@ -3091,11 +3091,11 @@
1.872      by (meson Diff_subset closure_subset subset_trans)
1.873  qed
1.874
1.875 -corollary simply_connected_punctured_universe:
1.876 +corollary%important simply_connected_punctured_universe:
1.877    fixes a :: "'a::euclidean_space"
1.878    assumes "3 \<le> DIM('a)"
1.879    shows "simply_connected(- {a})"
1.880 -proof -
1.881 +proof%unimportant -
1.882    have [simp]: "affine hull cball a 1 = UNIV"
1.883      apply auto
1.884      by (metis UNIV_I aff_dim_cball aff_dim_lt_full zero_less_one not_less_iff_gr_or_eq)
1.885 @@ -3109,12 +3109,12 @@
1.886  qed
1.887
1.888
1.889 -subsection\<open>The power, squaring and exponential functions as covering maps\<close>
1.890 -
1.891 -proposition covering_space_power_punctured_plane:
1.892 +subsection%important\<open>The power, squaring and exponential functions as covering maps\<close>
1.893 +
1.894 +proposition%important covering_space_power_punctured_plane:
1.895    assumes "0 < n"
1.896      shows "covering_space (- {0}) (\<lambda>z::complex. z^n) (- {0})"
1.897 -proof -
1.898 +proof%unimportant -
1.899    consider "n = 1" | "2 \<le> n" using assms by linarith
1.900    then obtain e where "0 < e"
1.901                  and e: "\<And>w z. cmod(w - z) < e * cmod z \<Longrightarrow> (w^n = z^n \<longleftrightarrow> w = z)"
1.902 @@ -3362,14 +3362,14 @@
1.903      done
1.904  qed
1.905
1.906 -corollary covering_space_square_punctured_plane:
1.907 +corollary%important covering_space_square_punctured_plane:
1.908    "covering_space (- {0}) (\<lambda>z::complex. z^2) (- {0})"
1.909 -  by (simp add: covering_space_power_punctured_plane)
1.910 -
1.911 -
1.912 -proposition covering_space_exp_punctured_plane:
1.913 +  by%unimportant (simp add: covering_space_power_punctured_plane)
1.914 +
1.915 +
1.916 +proposition%important covering_space_exp_punctured_plane:
1.917    "covering_space UNIV (\<lambda>z::complex. exp z) (- {0})"
1.918 -proof (simp add: covering_space_def, intro conjI ballI)
1.919 +proof%unimportant (simp add: covering_space_def, intro conjI ballI)
1.920    show "continuous_on UNIV (\<lambda>z::complex. exp z)"
1.921      by (rule continuous_on_exp [OF continuous_on_id])
1.922    show "range exp = - {0::complex}"
1.923 @@ -3483,9 +3483,9 @@
1.924  qed
1.925
1.926
1.927 -subsection\<open>Hence the Borsukian results about mappings into circles\<close>
1.928 -
1.929 -lemma inessential_eq_continuous_logarithm:
1.930 +subsection%important\<open>Hence the Borsukian results about mappings into circles\<close>
1.931 +
1.932 +lemma%unimportant inessential_eq_continuous_logarithm:
1.933    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.934    shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
1.935           (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x)))"
1.936 @@ -3509,7 +3509,7 @@
1.937      by (simp add: f homotopic_with_eq)
1.938  qed
1.939
1.940 -corollary inessential_imp_continuous_logarithm_circle:
1.941 +corollary%important inessential_imp_continuous_logarithm_circle:
1.942    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.943    assumes "homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)"
1.944    obtains g where "continuous_on S g" and "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
1.945 @@ -3521,7 +3521,7 @@
1.946  qed
1.947
1.948
1.949 -lemma inessential_eq_continuous_logarithm_circle:
1.950 +lemma%unimportant inessential_eq_continuous_logarithm_circle:
1.951    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.952    shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)) \<longleftrightarrow>
1.953           (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x))))"
1.954 @@ -3561,12 +3561,12 @@
1.956  qed
1.957
1.958 -lemma homotopic_with_sphere_times:
1.959 +lemma%important homotopic_with_sphere_times:
1.960    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.961    assumes hom: "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g" and conth: "continuous_on S h"
1.962        and hin: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> sphere 0 1"
1.963      shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x * h x) (\<lambda>x. g x * h x)"
1.964 -proof -
1.965 +proof%unimportant -
1.966    obtain k where contk: "continuous_on ({0..1::real} \<times> S) k"
1.967               and kim: "k ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
1.968               and k0:  "\<And>x. k(0, x) = f x"
1.969 @@ -3582,13 +3582,13 @@
1.970  qed
1.971
1.972
1.973 -lemma homotopic_circlemaps_divide:
1.974 +lemma%important homotopic_circlemaps_divide:
1.975    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.976      shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
1.977             continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
1.978             continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
1.979             (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c))"
1.980 -proof -
1.981 +proof%unimportant -
1.982    have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
1.983         if "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)" for c
1.984    proof -
1.985 @@ -3634,7 +3634,7 @@
1.987  qed
1.988
1.989 -subsection\<open>Upper and lower hemicontinuous functions\<close>
1.990 +subsection%important\<open>Upper and lower hemicontinuous functions\<close>
1.991
1.992  text\<open>And relation in the case of preimage map to open and closed maps, and fact that upper and lower
1.993  hemicontinuity together imply continuity in the sense of the Hausdorff metric (at points where the
1.994 @@ -3642,7 +3642,7 @@
1.995
1.996
1.997  text\<open>Many similar proofs below.\<close>
1.998 -lemma upper_hemicontinuous:
1.999 +lemma%unimportant upper_hemicontinuous:
1.1000    assumes "\<And>x. x \<in> S \<Longrightarrow> f x \<subseteq> T"
1.1001      shows "((\<forall>U. openin (subtopology euclidean T) U
1.1002                   \<longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<subseteq> U}) \<longleftrightarrow>
1.1003 @@ -3673,7 +3673,7 @@
1.1005  qed
1.1006
1.1007 -lemma lower_hemicontinuous:
1.1008 +lemma%unimportant lower_hemicontinuous:
1.1009    assumes "\<And>x. x \<in> S \<Longrightarrow> f x \<subseteq> T"
1.1010      shows "((\<forall>U. closedin (subtopology euclidean T) U
1.1011                   \<longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x \<subseteq> U}) \<longleftrightarrow>
1.1012 @@ -3704,7 +3704,7 @@
1.1014  qed
1.1015
1.1016 -lemma open_map_iff_lower_hemicontinuous_preimage:
1.1017 +lemma%unimportant open_map_iff_lower_hemicontinuous_preimage:
1.1018    assumes "f ` S \<subseteq> T"
1.1019      shows "((\<forall>U. openin (subtopology euclidean S) U
1.1020                   \<longrightarrow> openin (subtopology euclidean T) (f ` U)) \<longleftrightarrow>
1.1021 @@ -3735,7 +3735,7 @@
1.1022      using assms openin_imp_subset [OF opeSU] by (force simp: openin_closedin_eq)
1.1023  qed
1.1024
1.1025 -lemma closed_map_iff_upper_hemicontinuous_preimage:
1.1026 +lemma%unimportant closed_map_iff_upper_hemicontinuous_preimage:
1.1027    assumes "f ` S \<subseteq> T"
1.1028      shows "((\<forall>U. closedin (subtopology euclidean S) U
1.1029                   \<longrightarrow> closedin (subtopology euclidean T) (f ` U)) \<longleftrightarrow>
1.1030 @@ -3766,7 +3766,7 @@
1.1032  qed
1.1033
1.1034 -proposition upper_lower_hemicontinuous_explicit:
1.1035 +proposition%important upper_lower_hemicontinuous_explicit:
1.1036    fixes T :: "('b::{real_normed_vector,heine_borel}) set"
1.1037    assumes fST: "\<And>x. x \<in> S \<Longrightarrow> f x \<subseteq> T"
1.1038        and ope: "\<And>U. openin (subtopology euclidean T) U
1.1039 @@ -3778,7 +3778,7 @@
1.1040               "\<And>x'. \<lbrakk>x' \<in> S; dist x x' < d\<rbrakk>
1.1041                             \<Longrightarrow> (\<forall>y \<in> f x. \<exists>y'. y' \<in> f x' \<and> dist y y' < e) \<and>
1.1042                                 (\<forall>y' \<in> f x'. \<exists>y. y \<in> f x \<and> dist y' y < e)"
1.1043 -proof -
1.1044 +proof%unimportant -
1.1045    have "openin (subtopology euclidean T) (T \<inter> (\<Union>a\<in>f x. \<Union>b\<in>ball 0 e. {a + b}))"
1.1046      by (auto simp: open_sums openin_open_Int)
1.1047    with ope have "openin (subtopology euclidean S)
1.1048 @@ -3837,13 +3837,13 @@
1.1049  qed
1.1050
1.1051
1.1052 -subsection\<open>Complex logs exist on various "well-behaved" sets\<close>
1.1053 -
1.1054 -lemma continuous_logarithm_on_contractible:
1.1055 +subsection%important\<open>Complex logs exist on various "well-behaved" sets\<close>
1.1056 +
1.1057 +lemma%important continuous_logarithm_on_contractible:
1.1058    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.1059    assumes "continuous_on S f" "contractible S" "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
1.1060    obtains g where "continuous_on S g" "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
1.1061 -proof -
1.1062 +proof%unimportant -
1.1063    obtain c where hom: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>x. c)"
1.1064      using nullhomotopic_from_contractible assms
1.1065      by (metis imageE subset_Compl_singleton)
1.1066 @@ -3851,27 +3851,27 @@
1.1067      by (metis inessential_eq_continuous_logarithm that)
1.1068  qed
1.1069
1.1070 -lemma continuous_logarithm_on_simply_connected:
1.1071 +lemma%important continuous_logarithm_on_simply_connected:
1.1072    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.1073    assumes contf: "continuous_on S f" and S: "simply_connected S" "locally path_connected S"
1.1074        and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
1.1075    obtains g where "continuous_on S g" "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
1.1076 -  using covering_space_lift [OF covering_space_exp_punctured_plane S contf]
1.1077 -  by (metis (full_types) f imageE subset_Compl_singleton)
1.1078 -
1.1079 -lemma continuous_logarithm_on_cball:
1.1080 +  using%unimportant covering_space_lift [OF covering_space_exp_punctured_plane S contf]
1.1081 +  by%unimportant (metis (full_types) f imageE subset_Compl_singleton)
1.1082 +
1.1083 +lemma%unimportant continuous_logarithm_on_cball:
1.1084    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.1085    assumes "continuous_on (cball a r) f" and "\<And>z. z \<in> cball a r \<Longrightarrow> f z \<noteq> 0"
1.1086      obtains h where "continuous_on (cball a r) h" "\<And>z. z \<in> cball a r \<Longrightarrow> f z = exp(h z)"
1.1087    using assms continuous_logarithm_on_contractible convex_imp_contractible by blast
1.1088
1.1089 -lemma continuous_logarithm_on_ball:
1.1090 +lemma%unimportant continuous_logarithm_on_ball:
1.1091    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.1092    assumes "continuous_on (ball a r) f" and "\<And>z. z \<in> ball a r \<Longrightarrow> f z \<noteq> 0"
1.1093    obtains h where "continuous_on (ball a r) h" "\<And>z. z \<in> ball a r \<Longrightarrow> f z = exp(h z)"
1.1094    using assms continuous_logarithm_on_contractible convex_imp_contractible by blast
1.1095
1.1096 -lemma continuous_sqrt_on_contractible:
1.1097 +lemma%unimportant continuous_sqrt_on_contractible:
1.1098    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.1099    assumes "continuous_on S f" "contractible S"
1.1100        and "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
1.1101 @@ -3888,7 +3888,7 @@
1.1102    qed
1.1103  qed
1.1104
1.1105 -lemma continuous_sqrt_on_simply_connected:
1.1106 +lemma%unimportant continuous_sqrt_on_simply_connected:
1.1107    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
1.1108    assumes contf: "continuous_on S f" and S: "simply_connected S" "locally path_connected S"
1.1109        and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
1.1110 @@ -3906,14 +3906,14 @@
1.1111  qed
1.1112
1.1113
1.1114 -subsection\<open>Another simple case where sphere maps are nullhomotopic\<close>
1.1115 -
1.1116 -lemma inessential_spheremap_2_aux:
1.1117 +subsection%important\<open>Another simple case where sphere maps are nullhomotopic\<close>
1.1118 +
1.1119 +lemma%important inessential_spheremap_2_aux:
1.1120    fixes f :: "'a::euclidean_space \<Rightarrow> complex"
1.1121    assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f"
1.1122        and fim: "f `(sphere a r) \<subseteq> (sphere 0 1)"
1.1123    obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) f (\<lambda>x. c)"
1.1124 -proof -
1.1125 +proof%unimportant -
1.1126    obtain g where contg: "continuous_on (sphere a r) g"
1.1127               and feq: "\<And>x. x \<in> sphere a r \<Longrightarrow> f x = exp(g x)"
1.1128    proof (rule continuous_logarithm_on_simply_connected [OF contf])
1.1129 @@ -3935,12 +3935,12 @@
1.1130      by metis
1.1131  qed
1.1132
1.1133 -lemma inessential_spheremap_2:
1.1134 +lemma%important inessential_spheremap_2:
1.1135    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.1136    assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2"
1.1137        and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \<subseteq> (sphere b s)"
1.1138    obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
1.1139 -proof (cases "s \<le> 0")
1.1140 +proof%unimportant (cases "s \<le> 0")
1.1141    case True
1.1142    then show ?thesis
1.1143      using contf contractible_sphere fim nullhomotopic_into_contractible that by blast
1.1144 @@ -3972,14 +3972,14 @@
1.1145  qed
1.1146
1.1147
1.1148 -subsection\<open>Holomorphic logarithms and square roots\<close>
1.1149 -
1.1150 -lemma contractible_imp_holomorphic_log:
1.1151 +subsection%important\<open>Holomorphic logarithms and square roots\<close>
1.1152 +
1.1153 +lemma%important contractible_imp_holomorphic_log:
1.1154    assumes holf: "f holomorphic_on S"
1.1155        and S: "contractible S"
1.1156        and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
1.1157    obtains g where "g holomorphic_on S" "\<And>z. z \<in> S \<Longrightarrow> f z = exp(g z)"
1.1158 -proof -
1.1159 +proof%unimportant -
1.1160    have contf: "continuous_on S f"
1.1161      by (simp add: holf holomorphic_on_imp_continuous_on)
1.1162    obtain g where contg: "continuous_on S g" and feq: "\<And>x. x \<in> S \<Longrightarrow> f x = exp (g x)"
1.1163 @@ -4022,12 +4022,12 @@
1.1164  qed
1.1165
1.1166  (*Identical proofs*)
1.1167 -lemma simply_connected_imp_holomorphic_log:
1.1168 +lemma%important simply_connected_imp_holomorphic_log:
1.1169    assumes holf: "f holomorphic_on S"
1.1170        and S: "simply_connected S" "locally path_connected S"
1.1171        and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
1.1172    obtains g where "g holomorphic_on S" "\<And>z. z \<in> S \<Longrightarrow> f z = exp(g z)"
1.1173 -proof -
1.1174 +proof%unimportant -
1.1175    have contf: "continuous_on S f"
1.1176      by (simp add: holf holomorphic_on_imp_continuous_on)
1.1177    obtain g where contg: "continuous_on S g" and feq: "\<And>x. x \<in> S \<Longrightarrow> f x = exp (g x)"
1.1178 @@ -4070,7 +4070,7 @@
1.1179  qed
1.1180
1.1181
1.1182 -lemma contractible_imp_holomorphic_sqrt:
1.1183 +lemma%unimportant contractible_imp_holomorphic_sqrt:
1.1184    assumes holf: "f holomorphic_on S"
1.1185        and S: "contractible S"
1.1186        and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
1.1187 @@ -4088,7 +4088,7 @@
1.1188    qed
1.1189  qed
1.1190
1.1191 -lemma simply_connected_imp_holomorphic_sqrt:
1.1192 +lemma%unimportant simply_connected_imp_holomorphic_sqrt:
1.1193    assumes holf: "f holomorphic_on S"
1.1194        and S: "simply_connected S" "locally path_connected S"
1.1195        and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
1.1196 @@ -4108,11 +4108,11 @@
1.1197
1.1198  text\<open> Related theorems about holomorphic inverse cosines.\<close>
1.1199
1.1200 -lemma contractible_imp_holomorphic_arccos:
1.1201 +lemma%important contractible_imp_holomorphic_arccos:
1.1202    assumes holf: "f holomorphic_on S" and S: "contractible S"
1.1203        and non1: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1"
1.1204    obtains g where "g holomorphic_on S" "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)"
1.1205 -proof -
1.1206 +proof%unimportant -
1.1207    have hol1f: "(\<lambda>z. 1 - f z ^ 2) holomorphic_on S"
1.1208      by (intro holomorphic_intros holf)
1.1209    obtain g where holg: "g holomorphic_on S" and eq: "\<And>z. z \<in> S \<Longrightarrow> 1 - (f z)\<^sup>2 = (g z)\<^sup>2"
1.1210 @@ -4146,11 +4146,11 @@
1.1211  qed
1.1212
1.1213
1.1214 -lemma contractible_imp_holomorphic_arccos_bounded:
1.1215 +lemma%important contractible_imp_holomorphic_arccos_bounded:
1.1216    assumes holf: "f holomorphic_on S" and S: "contractible S" and "a \<in> S"
1.1217        and non1: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1"
1.1218    obtains g where "g holomorphic_on S" "norm(g a) \<le> pi + norm(f a)" "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)"
1.1219 -proof -
1.1220 +proof%unimportant -
1.1221    obtain g where holg: "g holomorphic_on S" and feq: "\<And>z. z \<in> S \<Longrightarrow> f z = cos (g z)"
1.1222      using contractible_imp_holomorphic_arccos [OF holf S non1] by blast
1.1223    obtain b where "cos b = f a" "norm b \<le> pi + norm (f a)"
1.1224 @@ -4186,21 +4186,21 @@
1.1225  qed
1.1226
1.1227
1.1228 -subsection\<open>The "Borsukian" property of sets\<close>
1.1229 +subsection%important\<open>The "Borsukian" property of sets\<close>
1.1230
1.1231  text\<open>This doesn't have a standard name. Kuratowski uses ``contractible with respect to \$[S^1]\$''
1.1232   while Whyburn uses ``property b''. It's closely related to unicoherence.\<close>
1.1233
1.1234 -definition Borsukian where
1.1235 +definition%important Borsukian where
1.1236      "Borsukian S \<equiv>
1.1237          \<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
1.1238              \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (- {0}) f (\<lambda>x. a))"
1.1239
1.1240 -lemma Borsukian_retraction_gen:
1.1241 +lemma%important Borsukian_retraction_gen:
1.1242    assumes "Borsukian S" "continuous_on S h" "h ` S = T"
1.1243            "continuous_on T k"  "k ` T \<subseteq> S"  "\<And>y. y \<in> T \<Longrightarrow> h(k y) = y"
1.1244      shows "Borsukian T"
1.1245 -proof -
1.1246 +proof%unimportant -
1.1247    interpret R: Retracts S h T k
1.1248      using assms by (simp add: Retracts.intro)
1.1249    show ?thesis
1.1250 @@ -4210,42 +4210,42 @@
1.1251      done
1.1252  qed
1.1253
1.1254 -lemma retract_of_Borsukian: "\<lbrakk>Borsukian T; S retract_of T\<rbrakk> \<Longrightarrow> Borsukian S"
1.1255 +lemma%unimportant retract_of_Borsukian: "\<lbrakk>Borsukian T; S retract_of T\<rbrakk> \<Longrightarrow> Borsukian S"
1.1256    apply (auto simp: retract_of_def retraction_def)
1.1257    apply (erule (1) Borsukian_retraction_gen)
1.1258    apply (meson retraction retraction_def)
1.1259      apply (auto simp: continuous_on_id)
1.1260      done
1.1261
1.1262 -lemma homeomorphic_Borsukian: "\<lbrakk>Borsukian S; S homeomorphic T\<rbrakk> \<Longrightarrow> Borsukian T"
1.1263 +lemma%unimportant homeomorphic_Borsukian: "\<lbrakk>Borsukian S; S homeomorphic T\<rbrakk> \<Longrightarrow> Borsukian T"
1.1264    using Borsukian_retraction_gen order_refl
1.1265    by (fastforce simp add: homeomorphism_def homeomorphic_def)
1.1266
1.1267 -lemma homeomorphic_Borsukian_eq:
1.1268 +lemma%unimportant homeomorphic_Borsukian_eq:
1.1269     "S homeomorphic T \<Longrightarrow> Borsukian S \<longleftrightarrow> Borsukian T"
1.1270    by (meson homeomorphic_Borsukian homeomorphic_sym)
1.1271
1.1272 -lemma Borsukian_translation:
1.1273 +lemma%unimportant Borsukian_translation:
1.1274    fixes S :: "'a::real_normed_vector set"
1.1275    shows "Borsukian (image (\<lambda>x. a + x) S) \<longleftrightarrow> Borsukian S"
1.1276    apply (rule homeomorphic_Borsukian_eq)
1.1277      using homeomorphic_translation homeomorphic_sym by blast
1.1278
1.1279 -lemma Borsukian_injective_linear_image:
1.1280 +lemma%unimportant Borsukian_injective_linear_image:
1.1281    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.1282    assumes "linear f" "inj f"
1.1283      shows "Borsukian(f ` S) \<longleftrightarrow> Borsukian S"
1.1284    apply (rule homeomorphic_Borsukian_eq)
1.1285    using assms homeomorphic_sym linear_homeomorphic_image by blast
1.1286
1.1287 -lemma homotopy_eqv_Borsukianness:
1.1288 +lemma%unimportant homotopy_eqv_Borsukianness:
1.1289    fixes S :: "'a::real_normed_vector set"
1.1290      and T :: "'b::real_normed_vector set"
1.1291     assumes "S homotopy_eqv T"
1.1292       shows "(Borsukian S \<longleftrightarrow> Borsukian T)"
1.1293    by (meson Borsukian_def assms homotopy_eqv_cohomotopic_triviality_null)
1.1294
1.1295 -lemma Borsukian_alt:
1.1296 +lemma%unimportant Borsukian_alt:
1.1297    fixes S :: "'a::real_normed_vector set"
1.1298    shows
1.1299     "Borsukian S \<longleftrightarrow>
1.1300 @@ -4255,20 +4255,20 @@
1.1301    unfolding Borsukian_def homotopic_triviality
1.1303
1.1304 -lemma Borsukian_continuous_logarithm:
1.1305 +lemma%unimportant Borsukian_continuous_logarithm:
1.1306    fixes S :: "'a::real_normed_vector set"
1.1307    shows "Borsukian S \<longleftrightarrow>
1.1308              (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
1.1309                   \<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))))"
1.1310    by (simp add: Borsukian_def inessential_eq_continuous_logarithm)
1.1311
1.1312 -lemma Borsukian_continuous_logarithm_circle:
1.1313 +lemma%important Borsukian_continuous_logarithm_circle:
1.1314    fixes S :: "'a::real_normed_vector set"
1.1315    shows "Borsukian S \<longleftrightarrow>
1.1316               (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
1.1317                    \<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))))"
1.1318     (is "?lhs = ?rhs")
1.1319 -proof
1.1320 +proof%unimportant
1.1321    assume ?lhs then show ?rhs
1.1322      by (force simp: Borsukian_continuous_logarithm)
1.1323  next
1.1324 @@ -4298,13 +4298,13 @@
1.1325  qed
1.1326
1.1327
1.1328 -lemma Borsukian_continuous_logarithm_circle_real:
1.1329 +lemma%important Borsukian_continuous_logarithm_circle_real:
1.1330    fixes S :: "'a::real_normed_vector set"
1.1331    shows "Borsukian S \<longleftrightarrow>
1.1332           (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
1.1333                \<longrightarrow> (\<exists>g. continuous_on S (complex_of_real \<circ> g) \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x)))))"
1.1334     (is "?lhs = ?rhs")
1.1335 -proof
1.1336 +proof%unimportant
1.1337    assume LHS: ?lhs
1.1338    show ?rhs
1.1339    proof (clarify)
1.1340 @@ -4331,52 +4331,52 @@
1.1341    qed
1.1342  qed
1.1343
1.1344 -lemma Borsukian_circle:
1.1345 +lemma%unimportant Borsukian_circle:
1.1346    fixes S :: "'a::real_normed_vector set"
1.1347    shows "Borsukian S \<longleftrightarrow>
1.1348           (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
1.1349                \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (sphere (0::complex) 1) f (\<lambda>x. a)))"
1.1350  by (simp add: inessential_eq_continuous_logarithm_circle Borsukian_continuous_logarithm_circle_real)
1.1351
1.1352 -lemma contractible_imp_Borsukian: "contractible S \<Longrightarrow> Borsukian S"
1.1353 +lemma%unimportant contractible_imp_Borsukian: "contractible S \<Longrightarrow> Borsukian S"
1.1354    by (meson Borsukian_def nullhomotopic_from_contractible)
1.1355
1.1356 -lemma simply_connected_imp_Borsukian:
1.1357 +lemma%unimportant simply_connected_imp_Borsukian:
1.1358    fixes S :: "'a::real_normed_vector set"
1.1359    shows  "\<lbrakk>simply_connected S; locally path_connected S\<rbrakk> \<Longrightarrow> Borsukian S"
1.1361    by (metis (no_types, lifting) continuous_logarithm_on_simply_connected image_iff)
1.1362
1.1363 -lemma starlike_imp_Borsukian:
1.1364 +lemma%unimportant starlike_imp_Borsukian:
1.1365    fixes S :: "'a::real_normed_vector set"
1.1366    shows "starlike S \<Longrightarrow> Borsukian S"
1.1367    by (simp add: contractible_imp_Borsukian starlike_imp_contractible)
1.1368
1.1369 -lemma Borsukian_empty: "Borsukian {}"
1.1370 +lemma%unimportant Borsukian_empty: "Borsukian {}"
1.1371    by (auto simp: contractible_imp_Borsukian)
1.1372
1.1373 -lemma Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)"
1.1374 +lemma%unimportant Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)"
1.1375    by (auto simp: contractible_imp_Borsukian)
1.1376
1.1377 -lemma convex_imp_Borsukian:
1.1378 +lemma%unimportant convex_imp_Borsukian:
1.1379    fixes S :: "'a::real_normed_vector set"
1.1380    shows "convex S \<Longrightarrow> Borsukian S"
1.1381    by (meson Borsukian_def convex_imp_contractible nullhomotopic_from_contractible)
1.1382
1.1383 -lemma Borsukian_sphere:
1.1384 +lemma%unimportant Borsukian_sphere:
1.1385    fixes a :: "'a::euclidean_space"
1.1386    shows "3 \<le> DIM('a) \<Longrightarrow> Borsukian (sphere a r)"
1.1387    apply (rule simply_connected_imp_Borsukian)
1.1388    using simply_connected_sphere apply blast
1.1389    using ENR_imp_locally_path_connected ENR_sphere by blast
1.1390
1.1391 -lemma Borsukian_open_Un:
1.1392 +lemma%important Borsukian_open_Un:
1.1393    fixes S :: "'a::real_normed_vector set"
1.1394    assumes opeS: "openin (subtopology euclidean (S \<union> T)) S"
1.1395        and opeT: "openin (subtopology euclidean (S \<union> T)) T"
1.1396        and BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S \<inter> T)"
1.1397      shows "Borsukian(S \<union> T)"
1.1398 -proof (clarsimp simp add: Borsukian_continuous_logarithm)
1.1399 +proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm)
1.1400    fix f :: "'a \<Rightarrow> complex"
1.1401    assume contf: "continuous_on (S \<union> T) f" and 0: "0 \<notin> f ` (S \<union> T)"
1.1402    then have contfS: "continuous_on S f" and contfT: "continuous_on T f"
1.1403 @@ -4440,13 +4440,13 @@
1.1404  qed
1.1405
1.1406  text\<open>The proof is a duplicate of that of \<open>Borsukian_open_Un\<close>.\<close>
1.1407 -lemma Borsukian_closed_Un:
1.1408 +lemma%important Borsukian_closed_Un:
1.1409    fixes S :: "'a::real_normed_vector set"
1.1410    assumes cloS: "closedin (subtopology euclidean (S \<union> T)) S"
1.1411        and cloT: "closedin (subtopology euclidean (S \<union> T)) T"
1.1412        and BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S \<inter> T)"
1.1413      shows "Borsukian(S \<union> T)"
1.1414 -proof (clarsimp simp add: Borsukian_continuous_logarithm)
1.1415 +proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm)
1.1416    fix f :: "'a \<Rightarrow> complex"
1.1417    assume contf: "continuous_on (S \<union> T) f" and 0: "0 \<notin> f ` (S \<union> T)"
1.1418    then have contfS: "continuous_on S f" and contfT: "continuous_on T f"
1.1419 @@ -4509,18 +4509,18 @@
1.1420    qed
1.1421  qed
1.1422
1.1423 -lemma Borsukian_separation_compact:
1.1424 +lemma%unimportant Borsukian_separation_compact:
1.1425    fixes S :: "complex set"
1.1426    assumes "compact S"
1.1427      shows "Borsukian S \<longleftrightarrow> connected(- S)"
1.1428    by (simp add: Borsuk_separation_theorem Borsukian_circle assms)
1.1429
1.1430 -lemma Borsukian_monotone_image_compact:
1.1431 +lemma%important Borsukian_monotone_image_compact:
1.1432    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.1433    assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T"
1.1434        and "compact S" and conn: "\<And>y. y \<in> T \<Longrightarrow> connected {x. x \<in> S \<and> f x = y}"
1.1435      shows "Borsukian T"
1.1436 -proof (clarsimp simp add: Borsukian_continuous_logarithm)
1.1437 +proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm)
1.1438    fix g :: "'b \<Rightarrow> complex"
1.1439    assume contg: "continuous_on T g" and 0: "0 \<notin> g ` T"
1.1440    have "continuous_on S (g \<circ> f)"
1.1441 @@ -4580,13 +4580,13 @@
1.1442  qed
1.1443
1.1444
1.1445 -lemma Borsukian_open_map_image_compact:
1.1446 +lemma%important Borsukian_open_map_image_compact:
1.1447    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.1448    assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T" and "compact S"
1.1449        and ope: "\<And>U. openin (subtopology euclidean S) U
1.1450                       \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
1.1451      shows "Borsukian T"
1.1452 -proof (clarsimp simp add: Borsukian_continuous_logarithm_circle_real)
1.1453 +proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm_circle_real)
1.1454    fix g :: "'b \<Rightarrow> complex"
1.1455    assume contg: "continuous_on T g" and gim: "g ` T \<subseteq> sphere 0 1"
1.1456    have "continuous_on S (g \<circ> f)"
1.1457 @@ -4667,12 +4667,12 @@
1.1458
1.1459
1.1460  text\<open>If two points are separated by a closed set, there's a minimal one.\<close>
1.1461 -proposition closed_irreducible_separator:
1.1462 +proposition%important closed_irreducible_separator:
1.1463    fixes a :: "'a::real_normed_vector"
1.1464    assumes "closed S" and ab: "\<not> connected_component (- S) a b"
1.1465    obtains T where "T \<subseteq> S" "closed T" "T \<noteq> {}" "\<not> connected_component (- T) a b"
1.1466                    "\<And>U. U \<subset> T \<Longrightarrow> connected_component (- U) a b"
1.1467 -proof (cases "a \<in> S \<or> b \<in> S")
1.1468 +proof%unimportant (cases "a \<in> S \<or> b \<in> S")
1.1469    case True
1.1470    then show ?thesis
1.1471    proof
1.1472 @@ -4775,7 +4775,7 @@
1.1473    qed
1.1474  qed
1.1475
1.1476 -lemma frontier_minimal_separating_closed_pointwise:
1.1477 +lemma%unimportant frontier_minimal_separating_closed_pointwise:
1.1478    fixes S :: "'a::real_normed_vector set"
1.1479    assumes S: "closed S" "a \<notin> S" and nconn: "\<not> connected_component (- S) a b"
1.1480        and conn: "\<And>T. \<lbrakk>closed T; T \<subset> S\<rbrakk> \<Longrightarrow> connected_component (- T) a b"
1.1481 @@ -4804,29 +4804,29 @@
1.1482  qed
1.1483
1.1484
1.1485 -subsection\<open>Unicoherence (closed)\<close>
1.1486 -
1.1487 -definition unicoherent where
1.1488 +subsection%important\<open>Unicoherence (closed)\<close>
1.1489 +
1.1490 +definition%important unicoherent where
1.1491    "unicoherent U \<equiv>
1.1492    \<forall>S T. connected S \<and> connected T \<and> S \<union> T = U \<and>
1.1493          closedin (subtopology euclidean U) S \<and> closedin (subtopology euclidean U) T
1.1494          \<longrightarrow> connected (S \<inter> T)"
1.1495
1.1496 -lemma unicoherentI [intro?]:
1.1497 +lemma%unimportant unicoherentI [intro?]:
1.1498    assumes "\<And>S T. \<lbrakk>connected S; connected T; U = S \<union> T; closedin (subtopology euclidean U) S; closedin (subtopology euclidean U) T\<rbrakk>
1.1499            \<Longrightarrow> connected (S \<inter> T)"
1.1500    shows "unicoherent U"
1.1501    using assms unfolding unicoherent_def by blast
1.1502
1.1503 -lemma unicoherentD:
1.1504 +lemma%unimportant unicoherentD:
1.1505    assumes "unicoherent U" "connected S" "connected T" "U = S \<union> T" "closedin (subtopology euclidean U) S" "closedin (subtopology euclidean U) T"
1.1506    shows "connected (S \<inter> T)"
1.1507    using assms unfolding unicoherent_def by blast
1.1508
1.1509 -lemma homeomorphic_unicoherent:
1.1510 +lemma%important homeomorphic_unicoherent:
1.1511    assumes ST: "S homeomorphic T" and S: "unicoherent S"
1.1512    shows "unicoherent T"
1.1513 -proof -
1.1514 +proof%unimportant -
1.1515    obtain f g where gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x" and fim: "T = f ` S" and gfim: "g ` f ` S = S"
1.1516      and contf: "continuous_on S f" and contg: "continuous_on (f ` S) g"
1.1517      using ST by (auto simp: homeomorphic_def homeomorphism_def)
1.1518 @@ -4867,24 +4867,24 @@
1.1519  qed
1.1520
1.1521
1.1522 -lemma homeomorphic_unicoherent_eq:
1.1523 +lemma%unimportant homeomorphic_unicoherent_eq:
1.1524     "S homeomorphic T \<Longrightarrow> (unicoherent S \<longleftrightarrow> unicoherent T)"
1.1525    by (meson homeomorphic_sym homeomorphic_unicoherent)
1.1526
1.1527 -lemma unicoherent_translation:
1.1528 +lemma%unimportant unicoherent_translation:
1.1529    fixes S :: "'a::real_normed_vector set"
1.1530    shows
1.1531     "unicoherent (image (\<lambda>x. a + x) S) \<longleftrightarrow> unicoherent S"
1.1532    using homeomorphic_translation homeomorphic_unicoherent_eq by blast
1.1533
1.1534 -lemma unicoherent_injective_linear_image:
1.1535 +lemma%unimportant unicoherent_injective_linear_image:
1.1536    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.1537    assumes "linear f" "inj f"
1.1538    shows "(unicoherent(f ` S) \<longleftrightarrow> unicoherent S)"
1.1539    using assms homeomorphic_unicoherent_eq linear_homeomorphic_image by blast
1.1540
1.1541
1.1542 -lemma Borsukian_imp_unicoherent:
1.1543 +lemma%unimportant Borsukian_imp_unicoherent:
1.1544    fixes U :: "'a::euclidean_space set"
1.1545    assumes "Borsukian U"  shows "unicoherent U"
1.1546    unfolding unicoherent_def
1.1547 @@ -4994,27 +4994,27 @@
1.1548  qed
1.1549
1.1550
1.1551 -corollary contractible_imp_unicoherent:
1.1552 +corollary%important contractible_imp_unicoherent:
1.1553    fixes U :: "'a::euclidean_space set"
1.1554    assumes "contractible U"  shows "unicoherent U"
1.1555 -  by (simp add: Borsukian_imp_unicoherent assms contractible_imp_Borsukian)
1.1556 -
1.1557 -corollary convex_imp_unicoherent:
1.1558 +  by%unimportant (simp add: Borsukian_imp_unicoherent assms contractible_imp_Borsukian)
1.1559 +
1.1560 +corollary%important convex_imp_unicoherent:
1.1561    fixes U :: "'a::euclidean_space set"
1.1562    assumes "convex U"  shows "unicoherent U"
1.1563 -  by (simp add: Borsukian_imp_unicoherent assms convex_imp_Borsukian)
1.1564 +  by%unimportant (simp add: Borsukian_imp_unicoherent assms convex_imp_Borsukian)
1.1565
1.1566  text\<open>If the type class constraint can be relaxed, I don't know how!\<close>
1.1567 -corollary unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)"
1.1568 -  by (simp add: convex_imp_unicoherent)
1.1569 -
1.1570 -
1.1571 -lemma unicoherent_monotone_image_compact:
1.1572 +corollary%important unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)"
1.1573 +  by%unimportant (simp add: convex_imp_unicoherent)
1.1574 +
1.1575 +
1.1576 +lemma%important unicoherent_monotone_image_compact:
1.1577    fixes T :: "'b :: t2_space set"
1.1578    assumes S: "unicoherent S" "compact S" and contf: "continuous_on S f" and fim: "f ` S = T"
1.1579    and conn: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
1.1580    shows "unicoherent T"
1.1581 -proof
1.1582 +proof%unimportant
1.1583    fix U V
1.1584    assume UV: "connected U" "connected V" "T = U \<union> V"
1.1585       and cloU: "closedin (subtopology euclidean T) U"
1.1586 @@ -5048,9 +5048,9 @@
1.1587  qed
1.1588
1.1589
1.1590 -subsection\<open>Several common variants of unicoherence\<close>
1.1591 -
1.1592 -lemma connected_frontier_simple:
1.1593 +subsection%important\<open>Several common variants of unicoherence\<close>
1.1594 +
1.1595 +lemma%unimportant connected_frontier_simple:
1.1596    fixes S :: "'a :: euclidean_space set"
1.1597    assumes "connected S" "connected(- S)" shows "connected(frontier S)"
1.1598    unfolding frontier_closures
1.1599 @@ -5058,18 +5058,18 @@
1.1600        apply (simp_all add: assms connected_imp_connected_closure)
1.1602
1.1603 -lemma connected_frontier_component_complement:
1.1604 +lemma%unimportant connected_frontier_component_complement:
1.1605    fixes S :: "'a :: euclidean_space set"
1.1606    assumes "connected S" and C: "C \<in> components(- S)" shows "connected(frontier C)"
1.1607    apply (rule connected_frontier_simple)
1.1608    using C in_components_connected apply blast
1.1609    by (metis Compl_eq_Diff_UNIV connected_UNIV assms top_greatest component_complement_connected)
1.1610
1.1611 -lemma connected_frontier_disjoint:
1.1612 +lemma%important connected_frontier_disjoint:
1.1613    fixes S :: "'a :: euclidean_space set"
1.1614    assumes "connected S" "connected T" "disjnt S T" and ST: "frontier S \<subseteq> frontier T"
1.1615    shows "connected(frontier S)"
1.1616 -proof (cases "S = UNIV")
1.1617 +proof%unimportant (cases "S = UNIV")
1.1618    case True then show ?thesis
1.1619      by simp
1.1620  next
1.1621 @@ -5101,13 +5101,13 @@
1.1622  qed
1.1623
1.1624
1.1625 -subsection\<open>Some separation results\<close>
1.1626 -
1.1627 -lemma separation_by_component_closed_pointwise:
1.1628 +subsection%important\<open>Some separation results\<close>
1.1629 +
1.1630 +lemma%important separation_by_component_closed_pointwise:
1.1631    fixes S :: "'a :: euclidean_space set"
1.1632    assumes "closed S" "\<not> connected_component (- S) a b"
1.1633    obtains C where "C \<in> components S" "\<not> connected_component(- C) a b"
1.1634 -proof (cases "a \<in> S \<or> b \<in> S")
1.1635 +proof%unimportant (cases "a \<in> S \<or> b \<in> S")
1.1636    case True
1.1637    then show ?thesis
1.1638      using connected_component_in componentsI that by fastforce
1.1639 @@ -5140,11 +5140,11 @@
1.1640  qed
1.1641
1.1642
1.1643 -lemma separation_by_component_closed:
1.1644 +lemma%important separation_by_component_closed:
1.1645    fixes S :: "'a :: euclidean_space set"
1.1646    assumes "closed S" "\<not> connected(- S)"
1.1647    obtains C where "C \<in> components S" "\<not> connected(- C)"
1.1648 -proof -
1.1649 +proof%unimportant -
1.1650    obtain x y where "closed S" "x \<notin> S" "y \<notin> S" and "\<not> connected_component (- S) x y"
1.1651      using assms by (auto simp: connected_iff_connected_component)
1.1652    then obtain C where "C \<in> components S" "\<not> connected_component(- C) x y"
1.1653 @@ -5154,12 +5154,12 @@
1.1654      by (metis Compl_iff \<open>C \<in> components S\<close> \<open>x \<notin> S\<close> \<open>y \<notin> S\<close> connected_component_eq connected_component_eq_eq connected_iff_connected_component that)
1.1655  qed
1.1656
1.1657 -lemma separation_by_Un_closed_pointwise:
1.1658 +lemma%important separation_by_Un_closed_pointwise:
1.1659    fixes S :: "'a :: euclidean_space set"
1.1660    assumes ST: "closed S" "closed T" "S \<inter> T = {}"
1.1661        and conS: "connected_component (- S) a b" and conT: "connected_component (- T) a b"
1.1662      shows "connected_component (- (S \<union> T)) a b"
1.1663 -proof (rule ccontr)
1.1664 +proof%unimportant (rule ccontr)
1.1665    have "a \<notin> S" "b \<notin> S" "a \<notin> T" "b \<notin> T"
1.1666      using conS conT connected_component_in by auto
1.1667    assume "\<not> connected_component (- (S \<union> T)) a b"
1.1668 @@ -5178,14 +5178,14 @@
1.1669      by (meson Compl_anti_mono C conS conT connected_component_of_subset)
1.1670  qed
1.1671
1.1672 -lemma separation_by_Un_closed:
1.1673 +lemma%unimportant separation_by_Un_closed:
1.1674    fixes S :: "'a :: euclidean_space set"
1.1675    assumes ST: "closed S" "closed T" "S \<inter> T = {}" and conS: "connected(- S)" and conT: "connected(- T)"
1.1676    shows "connected(- (S \<union> T))"
1.1677    using assms separation_by_Un_closed_pointwise
1.1678    by (fastforce simp add: connected_iff_connected_component)
1.1679
1.1680 -lemma open_unicoherent_UNIV:
1.1681 +lemma%unimportant open_unicoherent_UNIV:
1.1682    fixes S :: "'a :: euclidean_space set"
1.1683    assumes "open S" "open T" "connected S" "connected T" "S \<union> T = UNIV"
1.1684    shows "connected(S \<inter> T)"
1.1685 @@ -5196,7 +5196,7 @@
1.1686      by simp
1.1687  qed
1.1688
1.1689 -lemma separation_by_component_open_aux:
1.1690 +lemma%unimportant separation_by_component_open_aux:
1.1691    fixes S :: "'a :: euclidean_space set"
1.1692    assumes ST: "closed S" "closed T" "S \<inter> T = {}"
1.1693        and "S \<noteq> {}" "T \<noteq> {}"
1.1694 @@ -5276,11 +5276,11 @@
1.1695  qed
1.1696
1.1697
1.1698 -lemma separation_by_component_open:
1.1699 +lemma%important separation_by_component_open:
1.1700    fixes S :: "'a :: euclidean_space set"
1.1701    assumes "open S" and non: "\<not> connected(- S)"
1.1702    obtains C where "C \<in> components S" "\<not> connected(- C)"
1.1703 -proof -
1.1704 +proof%unimportant -
1.1705    obtain T U
1.1706      where "closed T" "closed U" and TU: "T \<union> U = - S" "T \<inter> U = {}" "T \<noteq> {}" "U \<noteq> {}"
1.1707      using assms by (auto simp: connected_closed_set closed_def)
1.1708 @@ -5303,18 +5303,18 @@
1.1709    qed
1.1710  qed
1.1711
1.1712 -lemma separation_by_Un_open:
1.1713 +lemma%unimportant separation_by_Un_open:
1.1714    fixes S :: "'a :: euclidean_space set"
1.1715    assumes "open S" "open T" "S \<inter> T = {}" and cS: "connected(-S)" and cT: "connected(-T)"
1.1716      shows "connected(- (S \<union> T))"
1.1717    using assms unicoherent_UNIV unfolding unicoherent_def by force
1.1718
1.1719
1.1720 -lemma nonseparation_by_component_eq:
1.1721 +lemma%important nonseparation_by_component_eq:
1.1722    fixes S :: "'a :: euclidean_space set"
1.1723    assumes "open S \<or> closed S"
1.1724    shows "((\<forall>C \<in> components S. connected(-C)) \<longleftrightarrow> connected(- S))" (is "?lhs = ?rhs")
1.1725 -proof
1.1726 +proof%unimportant
1.1727    assume ?lhs with assms show ?rhs
1.1728      by (meson separation_by_component_closed separation_by_component_open)
1.1729  next
1.1730 @@ -5324,13 +5324,13 @@
1.1731
1.1732
1.1733  text\<open>Another interesting equivalent of an inessential mapping into C-{0}\<close>
1.1734 -proposition inessential_eq_extensible:
1.1735 +proposition%important inessential_eq_extensible:
1.1736    fixes f :: "'a::euclidean_space \<Rightarrow> complex"
1.1737    assumes "closed S"
1.1738    shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
1.1739           (\<exists>g. continuous_on UNIV g \<and> (\<forall>x \<in> S. g x = f x) \<and> (\<forall>x. g x \<noteq> 0))"
1.1740       (is "?lhs = ?rhs")
1.1741 -proof
1.1742 +proof%unimportant
1.1743    assume ?lhs
1.1744    then obtain a where a: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)" ..
1.1745    show ?rhs
1.1746 @@ -5390,14 +5390,14 @@
1.1748  qed
1.1749
1.1750 -lemma inessential_on_clopen_Union:
1.1751 +lemma%important inessential_on_clopen_Union:
1.1752    fixes \<F> :: "'a::euclidean_space set set"
1.1753    assumes T: "path_connected T"
1.1754        and "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
1.1755        and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
1.1756        and hom: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)"
1.1757    obtains a where "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
1.1758 -proof (cases "\<Union>\<F> = {}")
1.1759 +proof%unimportant (cases "\<Union>\<F> = {}")
1.1760    case True
1.1761    with that show ?thesis
1.1762      by force
1.1763 @@ -5438,12 +5438,12 @@
1.1764    then show ?thesis ..
1.1765  qed
1.1766
1.1767 -lemma Janiszewski_dual:
1.1768 +lemma%important Janiszewski_dual:
1.1769    fixes S :: "complex set"
1.1770    assumes
1.1771     "compact S" "compact T" "connected S" "connected T" "connected(- (S \<union> T))"
1.1772   shows "connected(S \<inter> T)"
1.1773 -proof -
1.1774 +proof%unimportant -
1.1775    have ST: "compact (S \<union> T)"
1.1776      by (simp add: assms compact_Un)
1.1777    with Borsukian_imp_unicoherent [of "S \<union> T"] ST assms
```