src/HOL/Analysis/Further_Topology.thy
 changeset 66939 04678058308f parent 66884 c2128ab11f61 child 66941 c67bb79a0ceb
```     1.1 --- a/src/HOL/Analysis/Further_Topology.thy	Sun Oct 29 19:39:03 2017 +0100
1.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Mon Oct 30 16:02:59 2017 +0000
1.3 @@ -4589,4 +4589,788 @@
1.4      using fk gfh kTS by force
1.5  qed
1.6
1.7 +
1.8 +text\<open>If two points are separated by a closed set, there's a minimal one.\<close>
1.9 +proposition closed_irreducible_separator:
1.10 +  fixes a :: "'a::real_normed_vector"
1.11 +  assumes "closed S" and ab: "\<not> connected_component (- S) a b"
1.12 +  obtains T where "T \<subseteq> S" "closed T" "T \<noteq> {}" "\<not> connected_component (- T) a b"
1.13 +                  "\<And>U. U \<subset> T \<Longrightarrow> connected_component (- U) a b"
1.14 +proof (cases "a \<in> S \<or> b \<in> S")
1.15 +  case True
1.16 +  then show ?thesis
1.17 +  proof
1.18 +    assume *: "a \<in> S"
1.19 +    show ?thesis
1.20 +    proof
1.21 +      show "{a} \<subseteq> S"
1.22 +        using * by blast
1.23 +      show "\<not> connected_component (- {a}) a b"
1.24 +        using connected_component_in by auto
1.25 +      show "\<And>U. U \<subset> {a} \<Longrightarrow> connected_component (- U) a b"
1.26 +        by (metis connected_component_UNIV UNIV_I compl_bot_eq connected_component_eq_eq less_le_not_le subset_singletonD)
1.27 +    qed auto
1.28 +  next
1.29 +    assume *: "b \<in> S"
1.30 +    show ?thesis
1.31 +    proof
1.32 +      show "{b} \<subseteq> S"
1.33 +        using * by blast
1.34 +      show "\<not> connected_component (- {b}) a b"
1.35 +        using connected_component_in by auto
1.36 +      show "\<And>U. U \<subset> {b} \<Longrightarrow> connected_component (- U) a b"
1.37 +        by (metis connected_component_UNIV UNIV_I compl_bot_eq connected_component_eq_eq less_le_not_le subset_singletonD)
1.38 +    qed auto
1.39 +  qed
1.40 +next
1.41 +  case False
1.42 +  define A where "A \<equiv> connected_component_set (- S) a"
1.43 +  define B where "B \<equiv> connected_component_set (- (closure A)) b"
1.44 +  have "a \<in> A"
1.45 +    using False A_def by auto
1.46 +  have "b \<in> B"
1.47 +    unfolding A_def B_def closure_Un_frontier
1.48 +    using ab False \<open>closed S\<close> frontier_complement frontier_of_connected_component_subset frontier_subset_closed by force
1.49 +  have "frontier B \<subseteq> frontier (connected_component_set (- closure A) b)"
1.50 +    using B_def by blast
1.51 +  also have frsub: "... \<subseteq> frontier A"
1.52 +  proof -
1.53 +    have "\<And>A. closure (- closure (- A)) \<subseteq> closure A"
1.54 +      by (metis (no_types) closure_mono closure_subset compl_le_compl_iff double_compl)
1.55 +    then show ?thesis
1.56 +      by (metis (no_types) closure_closure double_compl frontier_closures frontier_of_connected_component_subset le_inf_iff subset_trans)
1.57 +  qed
1.58 +  finally have frBA: "frontier B \<subseteq> frontier A" .
1.59 +  show ?thesis
1.60 +  proof
1.61 +    show "frontier B \<subseteq> S"
1.62 +    proof -
1.63 +      have "frontier S \<subseteq> S"
1.64 +        by (simp add: \<open>closed S\<close> frontier_subset_closed)
1.65 +      then show ?thesis
1.66 +        using frsub frontier_complement frontier_of_connected_component_subset
1.67 +        unfolding A_def B_def by blast
1.68 +    qed
1.69 +    show "closed (frontier B)"
1.70 +      by simp
1.71 +    show "\<not> connected_component (- frontier B) a b"
1.72 +      unfolding connected_component_def
1.73 +    proof clarify
1.74 +      fix T
1.75 +      assume "connected T" and TB: "T \<subseteq> - frontier B" and "a \<in> T" and "b \<in> T"
1.76 +      have "a \<notin> B"
1.77 +        by (metis A_def B_def ComplD \<open>a \<in> A\<close> assms(1) closed_open connected_component_subset in_closure_connected_component set_mp)
1.78 +      have "T \<inter> B \<noteq> {}"
1.79 +        using \<open>b \<in> B\<close> \<open>b \<in> T\<close> by blast
1.80 +      moreover have "T - B \<noteq> {}"
1.81 +        using \<open>a \<notin> B\<close> \<open>a \<in> T\<close> by blast
1.82 +      ultimately show "False"
1.83 +        using connected_Int_frontier [of T B] TB \<open>connected T\<close> by blast
1.84 +    qed
1.85 +    moreover have "connected_component (- frontier B) a b" if "frontier B = {}"
1.86 +      apply (simp add: that)
1.87 +      using connected_component_eq_UNIV by blast
1.88 +    ultimately show "frontier B \<noteq> {}"
1.89 +      by blast
1.90 +    show "connected_component (- U) a b" if "U \<subset> frontier B" for U
1.91 +    proof -
1.92 +      obtain p where Usub: "U \<subseteq> frontier B" and p: "p \<in> frontier B" "p \<notin> U"
1.93 +        using \<open>U \<subset> frontier B\<close> by blast
1.94 +      show ?thesis
1.95 +        unfolding connected_component_def
1.96 +      proof (intro exI conjI)
1.97 +        have "connected ((insert p A) \<union> (insert p B))"
1.98 +        proof (rule connected_Un)
1.99 +          show "connected (insert p A)"
1.100 +            by (metis A_def IntD1 frBA \<open>p \<in> frontier B\<close> closure_insert closure_subset connected_connected_component connected_intermediate_closure frontier_closures insert_absorb subsetCE subset_insertI)
1.101 +          show "connected (insert p B)"
1.102 +            by (metis B_def IntD1 \<open>p \<in> frontier B\<close> closure_insert closure_subset connected_connected_component connected_intermediate_closure frontier_closures insert_absorb subset_insertI)
1.103 +        qed blast
1.104 +        then show "connected (insert p (B \<union> A))"
1.105 +          by (simp add: sup.commute)
1.106 +        have "A \<subseteq> - U"
1.107 +          using A_def Usub \<open>frontier B \<subseteq> S\<close> connected_component_subset by fastforce
1.108 +        moreover have "B \<subseteq> - U"
1.109 +          using B_def Usub connected_component_subset frBA frontier_closures by fastforce
1.110 +        ultimately show "insert p (B \<union> A) \<subseteq> - U"
1.111 +          using p by auto
1.112 +      qed (auto simp: \<open>a \<in> A\<close> \<open>b \<in> B\<close>)
1.113 +    qed
1.114 +  qed
1.115 +qed
1.116 +
1.117 +lemma frontier_minimal_separating_closed_pointwise:
1.118 +  fixes S :: "'a::real_normed_vector set"
1.119 +  assumes S: "closed S" "a \<notin> S" and nconn: "\<not> connected_component (- S) a b"
1.120 +      and conn: "\<And>T. \<lbrakk>closed T; T \<subset> S\<rbrakk> \<Longrightarrow> connected_component (- T) a b"
1.121 +    shows "frontier(connected_component_set (- S) a) = S" (is "?F = S")
1.122 +proof -
1.123 +  have "?F \<subseteq> S"
1.124 +    by (simp add: S componentsI frontier_of_components_closed_complement)
1.125 +  moreover have False if "?F \<subset> S"
1.126 +  proof -
1.127 +    have "connected_component (- ?F) a b"
1.128 +      by (simp add: conn that)
1.129 +    then obtain T where "connected T" "T \<subseteq> -?F" "a \<in> T" "b \<in> T"
1.130 +      by (auto simp: connected_component_def)
1.131 +    moreover have "T \<inter> ?F \<noteq> {}"
1.132 +    proof (rule connected_Int_frontier [OF \<open>connected T\<close>])
1.133 +      show "T \<inter> connected_component_set (- S) a \<noteq> {}"
1.134 +        using \<open>a \<notin> S\<close> \<open>a \<in> T\<close> by fastforce
1.135 +      show "T - connected_component_set (- S) a \<noteq> {}"
1.136 +        using \<open>b \<in> T\<close> nconn by blast
1.137 +    qed
1.138 +    ultimately show ?thesis
1.139 +      by blast
1.140 +  qed
1.141 +  ultimately show ?thesis
1.142 +    by blast
1.143 +qed
1.144 +
1.145 +
1.146 +subsection\<open>Unicoherence (closed)\<close>
1.147 +
1.148 +definition unicoherent where
1.149 +  "unicoherent U \<equiv>
1.150 +  \<forall>S T. connected S \<and> connected T \<and> S \<union> T = U \<and>
1.151 +        closedin (subtopology euclidean U) S \<and> closedin (subtopology euclidean U) T
1.152 +        \<longrightarrow> connected (S \<inter> T)"
1.153 +
1.154 +lemma unicoherentI [intro?]:
1.155 +  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.156 +          \<Longrightarrow> connected (S \<inter> T)"
1.157 +  shows "unicoherent U"
1.158 +  using assms unfolding unicoherent_def by blast
1.159 +
1.160 +lemma unicoherentD:
1.161 +  assumes "unicoherent U" "connected S" "connected T" "U = S \<union> T" "closedin (subtopology euclidean U) S" "closedin (subtopology euclidean U) T"
1.162 +  shows "connected (S \<inter> T)"
1.163 +  using assms unfolding unicoherent_def by blast
1.164 +
1.165 +lemma homeomorphic_unicoherent:
1.166 +  assumes ST: "S homeomorphic T" and S: "unicoherent S"
1.167 +  shows "unicoherent T"
1.168 +proof -
1.169 +  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.170 +    and contf: "continuous_on S f" and contg: "continuous_on (f ` S) g"
1.171 +    using ST by (auto simp: homeomorphic_def homeomorphism_def)
1.172 +  show ?thesis
1.173 +  proof
1.174 +    fix U V
1.175 +    assume "connected U" "connected V" and T: "T = U \<union> V"
1.176 +      and cloU: "closedin (subtopology euclidean T) U"
1.177 +      and cloV: "closedin (subtopology euclidean T) V"
1.178 +    have "f ` (g ` U \<inter> g ` V) \<subseteq> U" "f ` (g ` U \<inter> g ` V) \<subseteq> V"
1.179 +      using gf fim T by auto (metis UnCI image_iff)+
1.180 +    moreover have "U \<inter> V \<subseteq> f ` (g ` U \<inter> g ` V)"
1.181 +      using gf fim by (force simp: image_iff T)
1.182 +    ultimately have "U \<inter> V = f ` (g ` U \<inter> g ` V)" by blast
1.183 +    moreover have "connected (f ` (g ` U \<inter> g ` V))"
1.184 +    proof (rule connected_continuous_image)
1.185 +      show "continuous_on (g ` U \<inter> g ` V) f"
1.186 +        apply (rule continuous_on_subset [OF contf])
1.187 +        using T fim gfim by blast
1.188 +      show "connected (g ` U \<inter> g ` V)"
1.189 +      proof (intro conjI unicoherentD [OF S])
1.190 +        show "connected (g ` U)" "connected (g ` V)"
1.191 +          using \<open>connected U\<close> cloU \<open>connected V\<close> cloV
1.192 +          by (metis Topological_Spaces.connected_continuous_image closedin_imp_subset contg continuous_on_subset fim)+
1.193 +        show "S = g ` U \<union> g ` V"
1.194 +          using T fim gfim by auto
1.195 +        have hom: "homeomorphism T S g f"
1.196 +          by (simp add: contf contg fim gf gfim homeomorphism_def)
1.197 +        have "closedin (subtopology euclidean T) U" "closedin (subtopology euclidean T) V"
1.198 +          by (simp_all add: cloU cloV)
1.199 +        then show "closedin (subtopology euclidean S) (g ` U)"
1.200 +                  "closedin (subtopology euclidean S) (g ` V)"
1.201 +          by (blast intro: homeomorphism_imp_closed_map [OF hom])+
1.202 +      qed
1.203 +    qed
1.204 +    ultimately show "connected (U \<inter> V)" by metis
1.205 +  qed
1.206 +qed
1.207 +
1.208 +
1.209 +lemma homeomorphic_unicoherent_eq:
1.210 +   "S homeomorphic T \<Longrightarrow> (unicoherent S \<longleftrightarrow> unicoherent T)"
1.211 +  by (meson homeomorphic_sym homeomorphic_unicoherent)
1.212 +
1.213 +lemma unicoherent_translation:
1.214 +  fixes S :: "'a::real_normed_vector set"
1.215 +  shows
1.216 +   "unicoherent (image (\<lambda>x. a + x) S) \<longleftrightarrow> unicoherent S"
1.217 +  using homeomorphic_translation homeomorphic_unicoherent_eq by blast
1.218 +
1.219 +lemma unicoherent_injective_linear_image:
1.220 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.221 +  assumes "linear f" "inj f"
1.222 +  shows "(unicoherent(f ` S) \<longleftrightarrow> unicoherent S)"
1.223 +  using assms homeomorphic_unicoherent_eq linear_homeomorphic_image by blast
1.224 +
1.225 +
1.226 +lemma Borsukian_imp_unicoherent:
1.227 +  fixes U :: "'a::euclidean_space set"
1.228 +  assumes "Borsukian U"  shows "unicoherent U"
1.229 +  unfolding unicoherent_def
1.230 +proof clarify
1.231 +  fix S T
1.232 +  assume "connected S" "connected T" "U = S \<union> T"
1.233 +     and cloS: "closedin (subtopology euclidean (S \<union> T)) S"
1.234 +     and cloT: "closedin (subtopology euclidean (S \<union> T)) T"
1.235 +  show "connected (S \<inter> T)"
1.236 +    unfolding connected_closedin_eq
1.237 +  proof clarify
1.238 +    fix V W
1.239 +    assume "closedin (subtopology euclidean (S \<inter> T)) V"
1.240 +       and "closedin (subtopology euclidean (S \<inter> T)) W"
1.241 +       and VW: "V \<union> W = S \<inter> T" "V \<inter> W = {}" and "V \<noteq> {}" "W \<noteq> {}"
1.242 +    then have cloV: "closedin (subtopology euclidean U) V" and cloW: "closedin (subtopology euclidean U) W"
1.243 +      using \<open>U = S \<union> T\<close> cloS cloT closedin_trans by blast+
1.244 +    obtain q where contq: "continuous_on U q"
1.245 +         and q01: "\<And>x. x \<in> U \<Longrightarrow> q x \<in> {0..1::real}"
1.246 +         and qV: "\<And>x. x \<in> V \<Longrightarrow> q x = 0" and qW: "\<And>x. x \<in> W \<Longrightarrow> q x = 1"
1.247 +      by (rule Urysohn_local [OF cloV cloW \<open>V \<inter> W = {}\<close>, of 0 1])
1.248 +         (fastforce simp: closed_segment_eq_real_ivl)
1.249 +    let ?h = "\<lambda>x. if x \<in> S then exp(pi * \<i> * q x) else 1 / exp(pi * \<i> * q x)"
1.250 +    have eqST: "exp(pi * \<i> * q x) = 1 / exp(pi * \<i> * q x)" if "x \<in> S \<inter> T" for x
1.251 +    proof -
1.252 +      have "x \<in> V \<union> W"
1.253 +        using that \<open>V \<union> W = S \<inter> T\<close> by blast
1.254 +      with qV qW show ?thesis by force
1.255 +    qed
1.256 +    obtain g where contg: "continuous_on U g"
1.257 +      and circle: "g ` U \<subseteq> sphere 0 1"
1.258 +      and S: "\<And>x. x \<in> S \<Longrightarrow> g x = exp(pi * \<i> * q x)"
1.259 +      and T: "\<And>x. x \<in> T \<Longrightarrow> g x = 1 / exp(pi * \<i> * q x)"
1.260 +    proof
1.261 +      show "continuous_on U ?h"
1.262 +        unfolding \<open>U = S \<union> T\<close>
1.263 +      proof (rule continuous_on_cases_local [OF cloS cloT])
1.264 +        show "continuous_on S (\<lambda>x. exp (pi * \<i> * q x))"
1.265 +          apply (intro continuous_intros)
1.266 +          using \<open>U = S \<union> T\<close> continuous_on_subset contq by blast
1.267 +        show "continuous_on T (\<lambda>x. 1 / exp (pi * \<i> * q x))"
1.268 +          apply (intro continuous_intros)
1.269 +          using \<open>U = S \<union> T\<close> continuous_on_subset contq by auto
1.270 +      qed (use eqST in auto)
1.271 +    qed (use eqST in \<open>auto simp: norm_divide\<close>)
1.272 +    then obtain h where conth: "continuous_on U h" and heq: "\<And>x. x \<in> U \<Longrightarrow> g x = exp (h x)"
1.273 +      by (metis Borsukian_continuous_logarithm_circle assms)
1.274 +    obtain v w where "v \<in> V" "w \<in> W"
1.275 +      using \<open>V \<noteq> {}\<close> \<open>W \<noteq> {}\<close> by blast
1.276 +    then have vw: "v \<in> S \<inter> T" "w \<in> S \<inter> T"
1.277 +      using VW by auto
1.278 +    have iff: "2 * pi \<le> cmod (2 * of_int m * of_real pi * \<i> - 2 * of_int n * of_real pi * \<i>)
1.279 +          \<longleftrightarrow> 1 \<le> abs (m - n)" for m n
1.280 +    proof -
1.281 +      have "2 * pi \<le> cmod (2 * of_int m * of_real pi * \<i> - 2 * of_int n * of_real pi * \<i>)
1.282 +            \<longleftrightarrow> 2 * pi \<le> cmod ((2 * pi * \<i>) * (of_int m - of_int n))"
1.283 +        by (simp add: algebra_simps)
1.284 +      also have "... \<longleftrightarrow> 2 * pi \<le> 2 * pi * cmod (of_int m - of_int n)"
1.285 +        by (simp add: norm_mult)
1.286 +      also have "... \<longleftrightarrow> 1 \<le> abs (m - n)"
1.287 +        by simp (metis norm_of_int of_int_1_le_iff of_int_abs of_int_diff)
1.288 +      finally show ?thesis .
1.289 +    qed
1.290 +    have *: "\<exists>n::int. h x - (pi * \<i> * q x) = (of_int(2*n) * pi) * \<i>" if "x \<in> S" for x
1.291 +      using that S \<open>U = S \<union> T\<close> heq exp_eq [symmetric] by (simp add: algebra_simps)
1.292 +    moreover have "(\<lambda>x. h x - (pi * \<i> * q x)) constant_on S"
1.293 +    proof (rule continuous_discrete_range_constant [OF \<open>connected S\<close>])
1.294 +      have "continuous_on S h" "continuous_on S q"
1.295 +        using \<open>U = S \<union> T\<close> continuous_on_subset conth contq by blast+
1.296 +      then show "continuous_on S (\<lambda>x. h x - (pi * \<i> * q x))"
1.297 +        by (intro continuous_intros)
1.298 +      have "2*pi \<le> cmod (h y - (pi * \<i> * q y) - (h x - (pi * \<i> * q x)))"
1.299 +        if "x \<in> S" "y \<in> S" and ne: "h y - (pi * \<i> * q y) \<noteq> h x - (pi * \<i> * q x)" for x y
1.300 +        using * [OF \<open>x \<in> S\<close>] * [OF \<open>y \<in> S\<close>] ne by (auto simp: iff)
1.301 +      then show "\<And>x. x \<in> S \<Longrightarrow>
1.302 +         \<exists>e>0. \<forall>y. y \<in> S \<and> h y - (pi * \<i> * q y) \<noteq> h x - (pi * \<i> * q x) \<longrightarrow>
1.303 +                   e \<le> cmod (h y - (pi * \<i> * q y) - (h x - (pi * \<i> * q x)))"
1.304 +        by (rule_tac x="2*pi" in exI) auto
1.305 +    qed
1.306 +    ultimately
1.307 +    obtain m where m: "\<And>x. x \<in> S \<Longrightarrow> h x - (pi * \<i> * q x) = (of_int(2*m) * pi) * \<i>"
1.308 +      using vw by (force simp: constant_on_def)
1.309 +    have *: "\<exists>n::int. h x = - (pi * \<i> * q x) + (of_int(2*n) * pi) * \<i>" if "x \<in> T" for x
1.310 +      unfolding exp_eq [symmetric]
1.311 +      using that T \<open>U = S \<union> T\<close> by (simp add: exp_minus field_simps  heq [symmetric])
1.312 +    moreover have "(\<lambda>x. h x + (pi * \<i> * q x)) constant_on T"
1.313 +    proof (rule continuous_discrete_range_constant [OF \<open>connected T\<close>])
1.314 +      have "continuous_on T h" "continuous_on T q"
1.315 +        using \<open>U = S \<union> T\<close> continuous_on_subset conth contq by blast+
1.316 +      then show "continuous_on T (\<lambda>x. h x + (pi * \<i> * q x))"
1.317 +        by (intro continuous_intros)
1.318 +      have "2*pi \<le> cmod (h y + (pi * \<i> * q y) - (h x + (pi * \<i> * q x)))"
1.319 +        if "x \<in> T" "y \<in> T" and ne: "h y + (pi * \<i> * q y) \<noteq> h x + (pi * \<i> * q x)" for x y
1.320 +        using * [OF \<open>x \<in> T\<close>] * [OF \<open>y \<in> T\<close>] ne by (auto simp: iff)
1.321 +      then show "\<And>x. x \<in> T \<Longrightarrow>
1.322 +         \<exists>e>0. \<forall>y. y \<in> T \<and> h y + (pi * \<i> * q y) \<noteq> h x + (pi * \<i> * q x) \<longrightarrow>
1.323 +                   e \<le> cmod (h y + (pi * \<i> * q y) - (h x + (pi * \<i> * q x)))"
1.324 +        by (rule_tac x="2*pi" in exI) auto
1.325 +    qed
1.326 +    ultimately
1.327 +    obtain n where n: "\<And>x. x \<in> T \<Longrightarrow> h x + (pi * \<i> * q x) = (of_int(2*n) * pi) * \<i>"
1.328 +      using vw by (force simp: constant_on_def)
1.329 +    show "False"
1.330 +      using m [of v] m [of w] n [of v] n [of w] vw
1.331 +      by (auto simp: algebra_simps \<open>v \<in> V\<close> \<open>w \<in> W\<close> qV qW)
1.332 +  qed
1.333 +qed
1.334 +
1.335 +
1.336 +corollary contractible_imp_unicoherent:
1.337 +  fixes U :: "'a::euclidean_space set"
1.338 +  assumes "contractible U"  shows "unicoherent U"
1.339 +  by (simp add: Borsukian_imp_unicoherent assms contractible_imp_Borsukian)
1.340 +
1.341 +corollary convex_imp_unicoherent:
1.342 +  fixes U :: "'a::euclidean_space set"
1.343 +  assumes "convex U"  shows "unicoherent U"
1.344 +  by (simp add: Borsukian_imp_unicoherent assms convex_imp_Borsukian)
1.345 +
1.346 +text\<open>If the type class constraint can be relaxed, I don't know how!\<close>
1.347 +corollary unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)"
1.348 +  by (simp add: convex_imp_unicoherent)
1.349 +
1.350 +
1.351 +lemma unicoherent_monotone_image_compact:
1.352 +  fixes T :: "'b :: t2_space set"
1.353 +  assumes S: "unicoherent S" "compact S" and contf: "continuous_on S f" and fim: "f ` S = T"
1.354 +  and conn: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
1.355 +  shows "unicoherent T"
1.356 +proof
1.357 +  fix U V
1.358 +  assume UV: "connected U" "connected V" "T = U \<union> V"
1.359 +     and cloU: "closedin (subtopology euclidean T) U"
1.360 +     and cloV: "closedin (subtopology euclidean T) V"
1.361 +  moreover have "compact T"
1.362 +    using \<open>compact S\<close> compact_continuous_image contf fim by blast
1.363 +  ultimately have "closed U" "closed V"
1.364 +    by (auto simp: closedin_closed_eq compact_imp_closed)
1.365 +  let ?SUV = "(S \<inter> f -` U) \<inter> (S \<inter> f -` V)"
1.366 +  have UV_eq: "f ` ?SUV = U \<inter> V"
1.367 +    using \<open>T = U \<union> V\<close> fim by force+
1.368 +  have "connected (f ` ?SUV)"
1.369 +  proof (rule connected_continuous_image)
1.370 +    show "continuous_on ?SUV f"
1.371 +      by (meson contf continuous_on_subset inf_le1)
1.372 +    show "connected ?SUV"
1.373 +    proof (rule unicoherentD [OF \<open>unicoherent S\<close>, of "S \<inter> f -` U" "S \<inter> f -` V"])
1.374 +      have "\<And>C. closedin (subtopology euclidean S) C \<Longrightarrow> closedin (subtopology euclidean T) (f ` C)"
1.375 +        by (metis \<open>compact S\<close> closed_subset closedin_compact closedin_imp_subset compact_continuous_image compact_imp_closed contf continuous_on_subset fim image_mono)
1.376 +      then show "connected (S \<inter> f -` U)" "connected (S \<inter> f -` V)"
1.377 +        using UV by (auto simp: conn intro: connected_closed_monotone_preimage [OF contf fim])
1.378 +      show "S = (S \<inter> f -` U) \<union> (S \<inter> f -` V)"
1.379 +        using UV fim by blast
1.380 +      show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
1.381 +            "closedin (subtopology euclidean S) (S \<inter> f -` V)"
1.382 +        by (auto simp: continuous_on_imp_closedin cloU cloV contf fim)
1.383 +    qed
1.384 +  qed
1.385 +  with UV_eq show "connected (U \<inter> V)"
1.386 +    by simp
1.387 +qed
1.388 +
1.389 +
1.390 +
1.391 +subsection\<open>Several common variants of unicoherence\<close>
1.392 +
1.393 +lemma connected_frontier_simple:
1.394 +  fixes S :: "'a :: euclidean_space set"
1.395 +  assumes "connected S" "connected(- S)" shows "connected(frontier S)"
1.396 +  unfolding frontier_closures
1.397 +  apply (rule unicoherentD [OF unicoherent_UNIV])
1.398 +      apply (simp_all add: assms connected_imp_connected_closure)
1.399 +  by (simp add: closure_def)
1.400 +
1.401 +lemma connected_frontier_component_complement:
1.402 +  fixes S :: "'a :: euclidean_space set"
1.403 +  assumes "connected S" and C: "C \<in> components(- S)" shows "connected(frontier C)"
1.404 +  apply (rule connected_frontier_simple)
1.405 +  using C in_components_connected apply blast
1.406 +  by (metis Compl_eq_Diff_UNIV connected_UNIV assms top_greatest component_complement_connected)
1.407 +
1.408 +lemma connected_frontier_disjoint:
1.409 +  fixes S :: "'a :: euclidean_space set"
1.410 +  assumes "connected S" "connected T" "disjnt S T" and ST: "frontier S \<subseteq> frontier T"
1.411 +  shows "connected(frontier S)"
1.412 +proof (cases "S = UNIV")
1.413 +  case True then show ?thesis
1.414 +    by simp
1.415 +next
1.416 +  case False
1.417 +  then have "-S \<noteq> {}"
1.418 +    by blast
1.419 +  then obtain C where C: "C \<in> components(- S)" and "T \<subseteq> C"
1.420 +    by (metis ComplI disjnt_iff subsetI exists_component_superset \<open>disjnt S T\<close> \<open>connected T\<close>)
1.421 +  moreover have "frontier S = frontier C"
1.422 +  proof -
1.423 +    have "frontier C \<subseteq> frontier S"
1.424 +      using C frontier_complement frontier_of_components_subset by blast
1.425 +    moreover have "x \<in> frontier C" if "x \<in> frontier S" for x
1.426 +    proof -
1.427 +      have "x \<in> closure C"
1.428 +        using that unfolding frontier_def
1.429 +        by (metis (no_types) Diff_eq ST \<open>T \<subseteq> C\<close> closure_mono contra_subsetD frontier_def le_inf_iff that)
1.430 +      moreover have "x \<notin> interior C"
1.431 +        using that unfolding frontier_def
1.432 +        by (metis C Compl_eq_Diff_UNIV Diff_iff subsetD in_components_subset interior_diff interior_mono)
1.433 +      ultimately show ?thesis
1.434 +        by (auto simp: frontier_def)
1.435 +    qed
1.436 +    ultimately show ?thesis
1.437 +      by blast
1.438 +  qed
1.439 +  ultimately show ?thesis
1.440 +    using \<open>connected S\<close> connected_frontier_component_complement by auto
1.441 +qed
1.442 +
1.443 +lemma separation_by_component_closed_pointwise:
1.444 +  fixes S :: "'a :: euclidean_space set"
1.445 +  assumes "closed S" "\<not> connected_component (- S) a b"
1.446 +  obtains C where "C \<in> components S" "\<not> connected_component(- C) a b"
1.447 +proof (cases "a \<in> S \<or> b \<in> S")
1.448 +  case True
1.449 +  then show ?thesis
1.450 +    using connected_component_in componentsI that by fastforce
1.451 +next
1.452 +  case False
1.453 +  obtain T where "T \<subseteq> S" "closed T" "T \<noteq> {}"
1.454 +             and nab: "\<not> connected_component (- T) a b"
1.455 +             and conn: "\<And>U. U \<subset> T \<Longrightarrow> connected_component (- U) a b"
1.456 +    using closed_irreducible_separator [OF assms] by metis
1.457 +  moreover have "connected T"
1.458 +  proof -
1.459 +    have ab: "frontier(connected_component_set (- T) a) = T" "frontier(connected_component_set (- T) b) = T"
1.460 +      using frontier_minimal_separating_closed_pointwise
1.461 +      by (metis False \<open>T \<subseteq> S\<close> \<open>closed T\<close> connected_component_sym conn connected_component_eq_empty connected_component_intermediate_subset empty_subsetI nab)+
1.462 +    have "connected (frontier (connected_component_set (- T) a))"
1.463 +    proof (rule connected_frontier_disjoint)
1.464 +      show "disjnt (connected_component_set (- T) a) (connected_component_set (- T) b)"
1.465 +        unfolding disjnt_iff
1.466 +        by (metis connected_component_eq connected_component_eq_empty connected_component_idemp mem_Collect_eq nab)
1.467 +      show "frontier (connected_component_set (- T) a) \<subseteq> frontier (connected_component_set (- T) b)"
1.468 +        by (simp add: ab)
1.469 +    qed auto
1.470 +    with ab \<open>closed T\<close> show ?thesis
1.471 +      by simp
1.472 +  qed
1.473 +  ultimately obtain C where "C \<in> components S" "T \<subseteq> C"
1.474 +    using exists_component_superset [of T S] by blast
1.475 +  then show ?thesis
1.476 +    by (meson Compl_anti_mono connected_component_of_subset nab that)
1.477 +qed
1.478 +
1.479 +
1.480 +lemma separation_by_component_closed:
1.481 +  fixes S :: "'a :: euclidean_space set"
1.482 +  assumes "closed S" "\<not> connected(- S)"
1.483 +  obtains C where "C \<in> components S" "\<not> connected(- C)"
1.484 +proof -
1.485 +  obtain x y where "closed S" "x \<notin> S" "y \<notin> S" and "\<not> connected_component (- S) x y"
1.486 +    using assms by (auto simp: connected_iff_connected_component)
1.487 +  then obtain C where "C \<in> components S" "\<not> connected_component(- C) x y"
1.488 +    using separation_by_component_closed_pointwise by metis
1.489 +  then show "thesis"
1.490 +    apply (clarify elim!: componentsE)
1.491 +    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.492 +qed
1.493 +
1.494 +lemma separation_by_Un_closed_pointwise:
1.495 +  fixes S :: "'a :: euclidean_space set"
1.496 +  assumes ST: "closed S" "closed T" "S \<inter> T = {}"
1.497 +      and conS: "connected_component (- S) a b" and conT: "connected_component (- T) a b"
1.498 +    shows "connected_component (- (S \<union> T)) a b"
1.499 +proof (rule ccontr)
1.500 +  have "a \<notin> S" "b \<notin> S" "a \<notin> T" "b \<notin> T"
1.501 +    using conS conT connected_component_in by auto
1.502 +  assume "\<not> connected_component (- (S \<union> T)) a b"
1.503 +  then obtain C where "C \<in> components (S \<union> T)" and C: "\<not> connected_component(- C) a b"
1.504 +    using separation_by_component_closed_pointwise assms by blast
1.505 +  then have "C \<subseteq> S \<or> C \<subseteq> T"
1.506 +  proof -
1.507 +    have "connected C" "C \<subseteq> S \<union> T"
1.508 +      using \<open>C \<in> components (S \<union> T)\<close> in_components_subset by (blast elim: componentsE)+
1.509 +    moreover then have "C \<inter> T = {} \<or> C \<inter> S = {}"
1.510 +      by (metis Int_empty_right ST inf.commute connected_closed)
1.511 +    ultimately show ?thesis
1.512 +      by blast
1.513 +  qed
1.514 +  then show False
1.515 +    by (meson Compl_anti_mono C conS conT connected_component_of_subset)
1.516 +qed
1.517 +
1.518 +lemma separation_by_Un_closed:
1.519 +  fixes S :: "'a :: euclidean_space set"
1.520 +  assumes ST: "closed S" "closed T" "S \<inter> T = {}" and conS: "connected(- S)" and conT: "connected(- T)"
1.521 +  shows "connected(- (S \<union> T))"
1.522 +  using assms separation_by_Un_closed_pointwise
1.523 +  by (fastforce simp add: connected_iff_connected_component)
1.524 +
1.525 +lemma open_unicoherent_UNIV:
1.526 +  fixes S :: "'a :: euclidean_space set"
1.527 +  assumes "open S" "open T" "connected S" "connected T" "S \<union> T = UNIV"
1.528 +  shows "connected(S \<inter> T)"
1.529 +proof -
1.530 +  have "connected(- (-S \<union> -T))"
1.531 +    by (metis closed_Compl compl_sup compl_top_eq double_compl separation_by_Un_closed assms)
1.532 +  then show ?thesis
1.533 +    by simp
1.534 +qed
1.535 +
1.536 +lemma separation_by_component_open_aux:
1.537 +  fixes S :: "'a :: euclidean_space set"
1.538 +  assumes ST: "closed S" "closed T" "S \<inter> T = {}"
1.539 +      and "S \<noteq> {}" "T \<noteq> {}"
1.540 +  obtains C where "C \<in> components(-(S \<union> T))" "C \<noteq> {}" "frontier C \<inter> S \<noteq> {}" "frontier C \<inter> T \<noteq> {}"
1.541 +proof (rule ccontr)
1.542 +  let ?S = "S \<union> \<Union>{C \<in> components(- (S \<union> T)). frontier C \<subseteq> S}"
1.543 +  let ?T = "T \<union> \<Union>{C \<in> components(- (S \<union> T)). frontier C \<subseteq> T}"
1.544 +  assume "~ thesis"
1.545 +  with that have *: "frontier C \<inter> S = {} \<or> frontier C \<inter> T = {}"
1.546 +            if C: "C \<in> components (- (S \<union> T))" "C \<noteq> {}" for C
1.547 +    using C by blast
1.548 +  have "\<exists>A B::'a set. closed A \<and> closed B \<and> UNIV \<subseteq> A \<union> B \<and> A \<inter> B = {} \<and> A \<noteq> {} \<and> B \<noteq> {}"
1.549 +  proof (intro exI conjI)
1.550 +    have "frontier (\<Union>{C \<in> components (- S \<inter> - T). frontier C \<subseteq> S}) \<subseteq> S"
1.551 +      apply (rule subset_trans [OF frontier_Union_subset_closure])
1.552 +      by (metis (no_types, lifting) SUP_least \<open>closed S\<close> closure_minimal mem_Collect_eq)
1.553 +    then have "frontier ?S \<subseteq> S"
1.554 +      by (simp add: frontier_subset_eq assms  subset_trans [OF frontier_Un_subset])
1.555 +    then show "closed ?S"
1.556 +      using frontier_subset_eq by fastforce
1.557 +    have "frontier (\<Union>{C \<in> components (- S \<inter> - T). frontier C \<subseteq> T}) \<subseteq> T"
1.558 +      apply (rule subset_trans [OF frontier_Union_subset_closure])
1.559 +      by (metis (no_types, lifting) SUP_least \<open>closed T\<close> closure_minimal mem_Collect_eq)
1.560 +    then have "frontier ?T \<subseteq> T"
1.561 +      by (simp add: frontier_subset_eq assms  subset_trans [OF frontier_Un_subset])
1.562 +    then show "closed ?T"
1.563 +      using frontier_subset_eq by fastforce
1.564 +    have "UNIV \<subseteq> (S \<union> T) \<union> \<Union>(components(- (S \<union> T)))"
1.565 +      using Union_components by blast
1.566 +    also have "...  \<subseteq> ?S \<union> ?T"
1.567 +    proof -
1.568 +      have "C \<in> components (-(S \<union> T)) \<and> frontier C \<subseteq> S \<or>
1.569 +            C \<in> components (-(S \<union> T)) \<and> frontier C \<subseteq> T"
1.570 +        if "C \<in> components (- (S \<union> T))" "C \<noteq> {}" for C
1.571 +        using * [OF that] that
1.572 +        by clarify (metis (no_types, lifting) UnE \<open>closed S\<close> \<open>closed T\<close> closed_Un disjoint_iff_not_equal frontier_of_components_closed_complement subsetCE)
1.573 +      then show ?thesis
1.574 +        by blast
1.575 +    qed
1.576 +    finally show "UNIV \<subseteq> ?S \<union> ?T" .
1.577 +    have "\<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> S} \<union>
1.578 +          \<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> T} \<subseteq> - (S \<union> T)"
1.579 +      using in_components_subset by fastforce
1.580 +    moreover have "\<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> S} \<inter>
1.581 +                   \<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> T} = {}"
1.582 +    proof -
1.583 +      have "C \<inter> C' = {}" if "C \<in> components (- (S \<union> T))" "frontier C \<subseteq> S"
1.584 +                            "C' \<in> components (- (S \<union> T))" "frontier C' \<subseteq> T" for C C'
1.585 +      proof -
1.586 +        have NUN: "- S \<inter> - T \<noteq> UNIV"
1.587 +          using \<open>T \<noteq> {}\<close> by blast
1.588 +        have "C \<noteq> C'"
1.589 +        proof
1.590 +          assume "C = C'"
1.591 +          with that have "frontier C' \<subseteq> S \<inter> T"
1.592 +            by simp
1.593 +          also have "... = {}"
1.594 +            using \<open>S \<inter> T = {}\<close> by blast
1.595 +          finally have "C' = {} \<or> C' = UNIV"
1.596 +            using frontier_eq_empty by auto
1.597 +          then show False
1.598 +            using \<open>C = C'\<close> NUN that by (force simp: dest: in_components_nonempty in_components_subset)
1.599 +        qed
1.600 +        with that show ?thesis
1.601 +          by (simp add: components_nonoverlap [of _ "-(S \<union> T)"])
1.602 +      qed
1.603 +      then show ?thesis
1.604 +        by blast
1.605 +    qed
1.606 +    ultimately show "?S \<inter> ?T = {}"
1.607 +      using ST by blast
1.608 +    show "?S \<noteq> {}" "?T \<noteq> {}"
1.609 +      using \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> by blast+
1.610 +  qed
1.611 +    then show False
1.612 +      by (metis Compl_disjoint Convex_Euclidean_Space.connected_UNIV compl_bot_eq compl_unique connected_closedD inf_sup_absorb sup_compl_top_left1 top.extremum_uniqueI)
1.613 +qed
1.614 +
1.615 +
1.616 +lemma separation_by_component_open:
1.617 +  fixes S :: "'a :: euclidean_space set"
1.618 +  assumes "open S" and non: "\<not> connected(- S)"
1.619 +  obtains C where "C \<in> components S" "\<not> connected(- C)"
1.620 +proof -
1.621 +  obtain T U
1.622 +    where "closed T" "closed U" and TU: "T \<union> U = - S" "T \<inter> U = {}" "T \<noteq> {}" "U \<noteq> {}"
1.623 +    using assms by (auto simp: connected_closed_set closed_def)
1.624 +  then obtain C where C: "C \<in> components(-(T \<union> U))" "C \<noteq> {}"
1.625 +          and "frontier C \<inter> T \<noteq> {}" "frontier C \<inter> U \<noteq> {}"
1.626 +    using separation_by_component_open_aux [OF \<open>closed T\<close> \<open>closed U\<close> \<open>T \<inter> U = {}\<close>] by force
1.627 +  show "thesis"
1.628 +  proof
1.629 +    show "C \<in> components S"
1.630 +      using C(1) TU(1) by auto
1.631 +    show "\<not> connected (- C)"
1.632 +    proof
1.633 +      assume "connected (- C)"
1.634 +      then have "connected (frontier C)"
1.635 +        using connected_frontier_simple [of C] \<open>C \<in> components S\<close> in_components_connected by blast
1.636 +      then show False
1.637 +        unfolding connected_closed
1.638 +        by (metis C(1) TU(2) \<open>closed T\<close> \<open>closed U\<close> \<open>frontier C \<inter> T \<noteq> {}\<close> \<open>frontier C \<inter> U \<noteq> {}\<close> closed_Un frontier_of_components_closed_complement inf_bot_right inf_commute)
1.639 +    qed
1.640 +  qed
1.641 +qed
1.642 +
1.643 +lemma separation_by_Un_open:
1.644 +  fixes S :: "'a :: euclidean_space set"
1.645 +  assumes "open S" "open T" "S \<inter> T = {}" and cS: "connected(-S)" and cT: "connected(-T)"
1.646 +    shows "connected(- (S \<union> T))"
1.647 +  using assms unicoherent_UNIV unfolding unicoherent_def by force
1.648 +
1.649 +
1.650 +lemma nonseparation_by_component_eq:
1.651 +  fixes S :: "'a :: euclidean_space set"
1.652 +  assumes "open S \<or> closed S"
1.653 +  shows "((\<forall>C \<in> components S. connected(-C)) \<longleftrightarrow> connected(- S))" (is "?lhs = ?rhs")
1.654 +proof
1.655 +  assume ?lhs with assms show ?rhs
1.656 +    by (meson separation_by_component_closed separation_by_component_open)
1.657 +next
1.658 +  assume ?rhs with assms show ?lhs
1.659 +    using component_complement_connected by force
1.660 +qed
1.661 +
1.662 +
1.663 +text\<open>Another interesting equivalent of an inessential mapping into C-{0}\<close>
1.664 +proposition inessential_eq_extensible:
1.665 +  fixes f :: "'a::euclidean_space \<Rightarrow> complex"
1.666 +  assumes "closed S"
1.667 +  shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
1.668 +         (\<exists>g. continuous_on UNIV g \<and> (\<forall>x \<in> S. g x = f x) \<and> (\<forall>x. g x \<noteq> 0))"
1.669 +     (is "?lhs = ?rhs")
1.670 +proof
1.671 +  assume ?lhs
1.672 +  then obtain a where a: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)" ..
1.673 +  show ?rhs
1.674 +  proof (cases "S = {}")
1.675 +    case True
1.676 +    with a show ?thesis
1.677 +      using continuous_on_const by force
1.678 +  next
1.679 +    case False
1.680 +    have anr: "ANR (-{0::complex})"
1.681 +      by (simp add: ANR_delete open_Compl open_imp_ANR)
1.682 +    obtain g where contg: "continuous_on UNIV g" and gim: "g ` UNIV \<subseteq> -{0}"
1.683 +                   and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.684 +    proof (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ homotopic_with_symD [OF a]])
1.685 +      show "closedin (subtopology euclidean UNIV) S"
1.686 +        using assms by auto
1.687 +      show "range (\<lambda>t. a) \<subseteq> - {0}"
1.688 +        using a homotopic_with_imp_subset2 False by blast
1.689 +    qed (use anr that in \<open>force+\<close>)
1.690 +    then show ?thesis
1.691 +      by force
1.692 +  qed
1.693 +next
1.694 +  assume ?rhs
1.695 +  then obtain g where contg: "continuous_on UNIV g"
1.696 +          and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x" and non0: "\<And>x. g x \<noteq> 0"
1.697 +    by metis
1.698 +  obtain h k::"'a\<Rightarrow>'a" where hk: "homeomorphism (ball 0 1) UNIV h k"
1.699 +    using homeomorphic_ball01_UNIV homeomorphic_def by blast
1.700 +  then have "continuous_on (ball 0 1) (g \<circ> h)"
1.701 +    by (meson contg continuous_on_compose continuous_on_subset homeomorphism_cont1 top_greatest)
1.702 +  then obtain j where contj: "continuous_on (ball 0 1) j"
1.703 +                  and j: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> exp(j z) = (g \<circ> h) z"
1.704 +    by (metis (mono_tags, hide_lams) continuous_logarithm_on_ball comp_apply non0)
1.705 +  have [simp]: "\<And>x. x \<in> S \<Longrightarrow> h (k x) = x"
1.706 +    using hk homeomorphism_apply2 by blast
1.707 +  have "\<exists>\<zeta>. continuous_on S \<zeta>\<and> (\<forall>x\<in>S. f x = exp (\<zeta> x))"
1.708 +  proof (intro exI conjI ballI)
1.709 +    show "continuous_on S (j \<circ> k)"
1.710 +    proof (rule continuous_on_compose)
1.711 +      show "continuous_on S k"
1.712 +        by (meson continuous_on_subset hk homeomorphism_cont2 top_greatest)
1.713 +      show "continuous_on (k ` S) j"
1.714 +        apply (rule continuous_on_subset [OF contj])
1.715 +        using homeomorphism_image2 [OF hk] continuous_on_subset [OF contj] by blast
1.716 +    qed
1.717 +    show "f x = exp ((j \<circ> k) x)" if "x \<in> S" for x
1.718 +    proof -
1.719 +      have "f x = (g \<circ> h) (k x)"
1.720 +        by (simp add: gf that)
1.721 +      also have "... = exp (j (k x))"
1.722 +        by (metis rangeI homeomorphism_image2 [OF hk] j)
1.723 +      finally show ?thesis by simp
1.724 +    qed
1.725 +  qed
1.726 +  then show ?lhs
1.727 +    by (simp add: inessential_eq_continuous_logarithm)
1.728 +qed
1.729 +
1.730 +lemma inessential_on_clopen_Union:
1.731 +  fixes \<F> :: "'a::euclidean_space set set"
1.732 +  assumes T: "path_connected T"
1.733 +      and "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
1.734 +      and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
1.735 +      and hom: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)"
1.736 +  obtains a where "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
1.737 +proof (cases "\<Union>\<F> = {}")
1.738 +  case True
1.739 +  with that show ?thesis
1.740 +    by force
1.741 +next
1.742 +  case False
1.743 +  then obtain C where "C \<in> \<F>" "C \<noteq> {}"
1.744 +    by blast
1.745 +  then obtain a where clo: "closedin (subtopology euclidean (\<Union>\<F>)) C"
1.746 +    and ope: "openin (subtopology euclidean (\<Union>\<F>)) C"
1.747 +    and "homotopic_with (\<lambda>x. True) C T f (\<lambda>x. a)"
1.748 +    using assms by blast
1.749 +  with \<open>C \<noteq> {}\<close> have "f ` C \<subseteq> T" "a \<in> T"
1.750 +    using homotopic_with_imp_subset1 homotopic_with_imp_subset2 by blast+
1.751 +  have "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
1.752 +  proof (rule homotopic_on_clopen_Union)
1.753 +    show "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
1.754 +         "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
1.755 +      by (simp_all add: assms)
1.756 +    show "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)" if "S \<in> \<F>" for S
1.757 +    proof (cases "S = {}")
1.758 +      case True
1.759 +      then show ?thesis
1.760 +        by auto
1.761 +    next
1.762 +      case False
1.763 +      then obtain b where "b \<in> S"
1.764 +        by blast
1.765 +      obtain c where c: "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)"
1.766 +        using \<open>S \<in> \<F>\<close> hom by blast
1.767 +      then have "c \<in> T"
1.768 +        using \<open>b \<in> S\<close> homotopic_with_imp_subset2 by blast
1.769 +      then have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. c)"
1.770 +        using T \<open>a \<in> T\<close> homotopic_constant_maps path_connected_component by blast
1.771 +      then show ?thesis
1.772 +        using c homotopic_with_symD homotopic_with_trans by blast
1.773 +    qed
1.774 +  qed
1.775 +  then show ?thesis ..
1.776 +qed
1.777 +
1.778 +lemma Janiszewski_dual:
1.779 +  fixes S :: "complex set"
1.780 +  assumes
1.781 +   "compact S" "compact T" "connected S" "connected T" "connected(- (S \<union> T))"
1.782 + shows "connected(S \<inter> T)"
1.783 +proof -
1.784 +  have ST: "compact (S \<union> T)"
1.785 +    by (simp add: assms compact_Un)
1.786 +  with Borsukian_imp_unicoherent [of "S \<union> T"] ST assms
1.787 +  show ?thesis
1.788 +    by (auto simp: closed_subset compact_imp_closed Borsukian_separation_compact unicoherent_def)
1.789 +qed
1.790 +
1.791  end
```