# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1509379379 0
# Node ID 04678058308f78f52d8a8994cf954327efc9c55b
# Parent d0f12783cd80b3e63a5b1bc7e06b45e0ec0df6f5
New results in topology, mostly from HOL Light's moretop.ml
diff -r d0f12783cd80 -r 04678058308f src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Oct 29 19:39:03 2017 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Oct 30 16:02:59 2017 +0000
@@ -4446,6 +4446,46 @@
by (simp add: ENR_imp_ANR ENR_sphere)
+subsection\<open>Spheres are connected, etc.\<close>
+
+lemma locally_path_connected_sphere_gen:
+ fixes S :: "'a::euclidean_space set"
+ assumes "bounded S" and "convex S"
+ shows "locally path_connected (rel_frontier S)"
+proof (cases "rel_interior S = {}")
+ case True
+ with assms show ?thesis
+ by (simp add: rel_interior_eq_empty)
+next
+ case False
+ then obtain a where a: "a \<in> rel_interior S"
+ by blast
+ show ?thesis
+ proof (rule retract_of_locally_path_connected)
+ show "locally path_connected (affine hull S - {a})"
+ by (meson convex_affine_hull convex_imp_locally_path_connected locally_open_subset openin_delete openin_subtopology_self)
+ show "rel_frontier S retract_of affine hull S - {a}"
+ using a assms rel_frontier_retract_of_punctured_affine_hull by blast
+ qed
+qed
+
+lemma locally_connected_sphere_gen:
+ fixes S :: "'a::euclidean_space set"
+ assumes "bounded S" and "convex S"
+ shows "locally connected (rel_frontier S)"
+ by (simp add: ANR_imp_locally_connected ANR_rel_frontier_convex assms)
+
+lemma locally_path_connected_sphere:
+ fixes a :: "'a::euclidean_space"
+ shows "locally path_connected (sphere a r)"
+ using ENR_imp_locally_path_connected ENR_sphere by blast
+
+lemma locally_connected_sphere:
+ fixes a :: "'a::euclidean_space"
+ shows "locally connected(sphere a r)"
+ using ANR_imp_locally_connected ANR_sphere by blast
+
+
subsection\<open>Borsuk homotopy extension theorem\<close>
text\<open>It's only this late so we can use the concept of retraction,
@@ -4794,6 +4834,386 @@
qed
+subsection\<open>More extension theorems\<close>
+
+lemma extension_from_clopen:
+ assumes ope: "openin (subtopology euclidean S) T"
+ and clo: "closedin (subtopology euclidean S) T"
+ and contf: "continuous_on T f" and fim: "f ` T \<subseteq> U" and null: "U = {} \<Longrightarrow> S = {}"
+ obtains g where "continuous_on S g" "g ` S \<subseteq> U" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
+proof (cases "U = {}")
+ case True
+ then show ?thesis
+ by (simp add: null that)
+next
+ case False
+ then obtain a where "a \<in> U"
+ by auto
+ let ?g = "\<lambda>x. if x \<in> T then f x else a"
+ have Seq: "S = T \<union> (S - T)"
+ using clo closedin_imp_subset by fastforce
+ show ?thesis
+ proof
+ have "continuous_on (T \<union> (S - T)) ?g"
+ apply (rule continuous_on_cases_local)
+ using Seq clo ope by (auto simp: contf continuous_on_const intro: continuous_on_cases_local)
+ with Seq show "continuous_on S ?g"
+ by metis
+ show "?g ` S \<subseteq> U"
+ using \<open>a \<in> U\<close> fim by auto
+ show "\<And>x. x \<in> T \<Longrightarrow> ?g x = f x"
+ by auto
+ qed
+qed
+
+
+lemma extension_from_component:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+ assumes S: "locally connected S \<or> compact S" and "ANR U"
+ and C: "C \<in> components S" and contf: "continuous_on C f" and fim: "f ` C \<subseteq> U"
+ obtains g where "continuous_on S g" "g ` S \<subseteq> U" "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
+proof -
+ obtain T g where ope: "openin (subtopology euclidean S) T"
+ and clo: "closedin (subtopology euclidean S) T"
+ and "C \<subseteq> T" and contg: "continuous_on T g" and gim: "g ` T \<subseteq> U"
+ and gf: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
+ using S
+ proof
+ assume "locally connected S"
+ show ?thesis
+ by (metis C \<open>locally connected S\<close> openin_components_locally_connected closedin_component contf fim order_refl that)
+ next
+ assume "compact S"
+ then obtain W g where "C \<subseteq> W" and opeW: "openin (subtopology euclidean S) W"
+ and contg: "continuous_on W g"
+ and gim: "g ` W \<subseteq> U" and gf: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
+ using ANR_imp_absolute_neighbourhood_extensor [of U C f S] C \<open>ANR U\<close> closedin_component contf fim by blast
+ then obtain V where "open V" and V: "W = S \<inter> V"
+ by (auto simp: openin_open)
+ moreover have "locally compact S"
+ by (simp add: \<open>compact S\<close> closed_imp_locally_compact compact_imp_closed)
+ ultimately obtain K where opeK: "openin (subtopology euclidean S) K" and "compact K" "C \<subseteq> K" "K \<subseteq> V"
+ by (metis C Int_subset_iff \<open>C \<subseteq> W\<close> \<open>compact S\<close> compact_components Sura_Bura_clopen_subset)
+ show ?thesis
+ proof
+ show "closedin (subtopology euclidean S) K"
+ by (meson \<open>compact K\<close> \<open>compact S\<close> closedin_compact_eq opeK openin_imp_subset)
+ show "continuous_on K g"
+ by (metis Int_subset_iff V \<open>K \<subseteq> V\<close> contg continuous_on_subset opeK openin_subtopology subset_eq)
+ show "g ` K \<subseteq> U"
+ using V \<open>K \<subseteq> V\<close> gim opeK openin_imp_subset by fastforce
+ qed (use opeK gf \<open>C \<subseteq> K\<close> in auto)
+ qed
+ obtain h where "continuous_on S h" "h ` S \<subseteq> U" "\<And>x. x \<in> T \<Longrightarrow> h x = g x"
+ using extension_from_clopen
+ by (metis C bot.extremum_uniqueI clo contg gim fim image_is_empty in_components_nonempty ope)
+ then show ?thesis
+ by (metis \<open>C \<subseteq> T\<close> gf subset_eq that)
+qed
+
+
+lemma tube_lemma:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "compact S" and S: "S \<noteq> {}" "(\<lambda>x. (x,a)) ` S \<subseteq> U"
+ and ope: "openin (subtopology euclidean (S \<times> T)) U"
+ obtains V where "openin (subtopology euclidean T) V" "a \<in> V" "S \<times> V \<subseteq> U"
+proof -
+ let ?W = "{y. \<exists>x. x \<in> S \<and> (x, y) \<in> (S \<times> T - U)}"
+ have "U \<subseteq> S \<times> T" "closedin (subtopology euclidean (S \<times> T)) (S \<times> T - U)"
+ using ope by (auto simp: openin_closedin_eq)
+ then have "closedin (subtopology euclidean T) ?W"
+ using \<open>compact S\<close> closedin_compact_projection by blast
+ moreover have "a \<in> T - ?W"
+ using \<open>U \<subseteq> S \<times> T\<close> S by auto
+ moreover have "S \<times> (T - ?W) \<subseteq> U"
+ by auto
+ ultimately show ?thesis
+ by (metis (no_types, lifting) Sigma_cong closedin_def that topspace_euclidean_subtopology)
+qed
+
+lemma tube_lemma_gen:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "compact S" "S \<noteq> {}" "T \<subseteq> T'" "S \<times> T \<subseteq> U"
+ and ope: "openin (subtopology euclidean (S \<times> T')) U"
+ obtains V where "openin (subtopology euclidean T') V" "T \<subseteq> V" "S \<times> V \<subseteq> U"
+proof -
+ have "\<And>x. x \<in> T \<Longrightarrow> \<exists>V. openin (subtopology euclidean T') V \<and> x \<in> V \<and> S \<times> V \<subseteq> U"
+ using assms by (auto intro: tube_lemma [OF \<open>compact S\<close>])
+ then obtain F where F: "\<And>x. x \<in> T \<Longrightarrow> openin (subtopology euclidean T') (F x) \<and> x \<in> F x \<and> S \<times> F x \<subseteq> U"
+ by metis
+ show ?thesis
+ proof
+ show "openin (subtopology euclidean T') (UNION T F)"
+ using F by blast
+ show "T \<subseteq> UNION T F"
+ using F by blast
+ show "S \<times> UNION T F \<subseteq> U"
+ using F by auto
+ qed
+qed
+
+proposition homotopic_neighbourhood_extension:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> U"
+ and contg: "continuous_on S g" and gim: "g ` S \<subseteq> U"
+ and clo: "closedin (subtopology euclidean S) T"
+ and "ANR U" and hom: "homotopic_with (\<lambda>x. True) T U f g"
+ obtains V where "T \<subseteq> V" "openin (subtopology euclidean S) V"
+ "homotopic_with (\<lambda>x. True) V U f g"
+proof -
+ have "T \<subseteq> S"
+ using clo closedin_imp_subset by blast
+ obtain h where conth: "continuous_on ({0..1::real} \<times> T) h"
+ and him: "h ` ({0..1} \<times> T) \<subseteq> U"
+ and h0: "\<And>x. h(0, x) = f x" and h1: "\<And>x. h(1, x) = g x"
+ using hom by (auto simp: homotopic_with_def)
+ define h' where "h' \<equiv> \<lambda>z. if fst z \<in> {0} then f(snd z)
+ else if fst z \<in> {1} then g(snd z)
+ else h z"
+ let ?S0 = "{0::real} \<times> S" and ?S1 = "{1::real} \<times> S"
+ have "continuous_on(?S0 \<union> (?S1 \<union> {0..1} \<times> T)) h'"
+ unfolding h'_def
+ proof (intro continuous_on_cases_local)
+ show "closedin (subtopology euclidean (?S0 \<union> (?S1 \<union> {0..1} \<times> T))) ?S0"
+ "closedin (subtopology euclidean (?S1 \<union> {0..1} \<times> T)) ?S1"
+ using \<open>T \<subseteq> S\<close> by (force intro: closedin_Times closedin_subset_trans [of "{0..1} \<times> S"])+
+ show "closedin (subtopology euclidean (?S0 \<union> (?S1 \<union> {0..1} \<times> T))) (?S1 \<union> {0..1} \<times> T)"
+ "closedin (subtopology euclidean (?S1 \<union> {0..1} \<times> T)) ({0..1} \<times> T)"
+ using \<open>T \<subseteq> S\<close> by (force intro: clo closedin_Times closedin_subset_trans [of "{0..1} \<times> S"])+
+ show "continuous_on (?S0) (\<lambda>x. f (snd x))"
+ by (intro continuous_intros continuous_on_compose2 [OF contf]) auto
+ show "continuous_on (?S1) (\<lambda>x. g (snd x))"
+ by (intro continuous_intros continuous_on_compose2 [OF contg]) auto
+ qed (use h0 h1 conth in auto)
+ then have "continuous_on ({0,1} \<times> S \<union> ({0..1} \<times> T)) h'"
+ by (metis Sigma_Un_distrib1 Un_assoc insert_is_Un)
+ moreover have "h' ` ({0,1} \<times> S \<union> {0..1} \<times> T) \<subseteq> U"
+ using fim gim him \<open>T \<subseteq> S\<close> unfolding h'_def by force
+ moreover have "closedin (subtopology euclidean ({0..1::real} \<times> S)) ({0,1} \<times> S \<union> {0..1::real} \<times> T)"
+ by (intro closedin_Times closedin_Un clo) (simp_all add: closed_subset)
+ ultimately
+ obtain W k where W: "({0,1} \<times> S) \<union> ({0..1} \<times> T) \<subseteq> W"
+ and opeW: "openin (subtopology euclidean ({0..1} \<times> S)) W"
+ and contk: "continuous_on W k"
+ and kim: "k ` W \<subseteq> U"
+ and kh': "\<And>x. x \<in> ({0,1} \<times> S) \<union> ({0..1} \<times> T) \<Longrightarrow> k x = h' x"
+ by (metis ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR U\<close>, of "({0,1} \<times> S) \<union> ({0..1} \<times> T)" h' "{0..1} \<times> S"])
+ obtain T' where opeT': "openin (subtopology euclidean S) T'"
+ and "T \<subseteq> T'" and TW: "{0..1} \<times> T' \<subseteq> W"
+ using tube_lemma_gen [of "{0..1::real}" T S W] W \<open>T \<subseteq> S\<close> opeW by auto
+ moreover have "homotopic_with (\<lambda>x. True) T' U f g"
+ proof (simp add: homotopic_with, intro exI conjI)
+ show "continuous_on ({0..1} \<times> T') k"
+ using TW continuous_on_subset contk by auto
+ show "k ` ({0..1} \<times> T') \<subseteq> U"
+ using TW kim by fastforce
+ have "T' \<subseteq> S"
+ by (meson opeT' subsetD openin_imp_subset)
+ then show "\<forall>x\<in>T'. k (0, x) = f x" "\<forall>x\<in>T'. k (1, x) = g x"
+ by (auto simp: kh' h'_def)
+ qed
+ ultimately show ?thesis
+ by (blast intro: that)
+qed
+
+text\<open> Homotopy on a union of closed-open sets.\<close>
+proposition homotopic_on_clopen_Union:
+ fixes \<F> :: "'a::euclidean_space set set"
+ assumes "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
+ and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
+ and "\<And>S. S \<in> \<F> \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
+ shows "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f g"
+proof -
+ obtain \<V> where "\<V> \<subseteq> \<F>" "countable \<V>" and eqU: "\<Union>\<V> = \<Union>\<F>"
+ using Lindelof_openin assms by blast
+ show ?thesis
+ proof (cases "\<V> = {}")
+ case True
+ then show ?thesis
+ by (metis Union_empty eqU homotopic_on_empty)
+ next
+ case False
+ then obtain V :: "nat \<Rightarrow> 'a set" where V: "range V = \<V>"
+ using range_from_nat_into \<open>countable \<V>\<close> by metis
+ with \<open>\<V> \<subseteq> \<F>\<close> have clo: "\<And>n. closedin (subtopology euclidean (\<Union>\<F>)) (V n)"
+ and ope: "\<And>n. openin (subtopology euclidean (\<Union>\<F>)) (V n)"
+ and hom: "\<And>n. homotopic_with (\<lambda>x. True) (V n) T f g"
+ using assms by auto
+ then obtain h where conth: "\<And>n. continuous_on ({0..1::real} \<times> V n) (h n)"
+ and him: "\<And>n. h n ` ({0..1} \<times> V n) \<subseteq> T"
+ and h0: "\<And>n. \<And>x. x \<in> V n \<Longrightarrow> h n (0, x) = f x"
+ and h1: "\<And>n. \<And>x. x \<in> V n \<Longrightarrow> h n (1, x) = g x"
+ by (simp add: homotopic_with) metis
+ have wop: "b \<in> V x \<Longrightarrow> \<exists>k. b \<in> V k \<and> (\<forall>j<k. b \<notin> V j)" for b x
+ using nat_less_induct [where P = "\<lambda>i. b \<notin> V i"] by meson
+ obtain \<zeta> where cont: "continuous_on ({0..1} \<times> UNION UNIV V) \<zeta>"
+ and eq: "\<And>x i. \<lbrakk>x \<in> {0..1} \<times> UNION UNIV V \<inter>
+ {0..1} \<times> (V i - (\<Union>m<i. V m))\<rbrakk> \<Longrightarrow> \<zeta> x = h i x"
+ proof (rule pasting_lemma_exists)
+ show "{0..1} \<times> UNION UNIV V \<subseteq> (\<Union>i. {0..1::real} \<times> (V i - (\<Union>m<i. V m)))"
+ by (force simp: Ball_def dest: wop)
+ show "openin (subtopology euclidean ({0..1} \<times> UNION UNIV V))
+ ({0..1::real} \<times> (V i - (\<Union>m<i. V m)))" for i
+ proof (intro openin_Times openin_subtopology_self openin_diff)
+ show "openin (subtopology euclidean (UNION UNIV V)) (V i)"
+ using ope V eqU by auto
+ show "closedin (subtopology euclidean (UNION UNIV V)) (\<Union>m<i. V m)"
+ using V clo eqU by (force intro: closedin_Union)
+ qed
+ show "continuous_on ({0..1} \<times> (V i - (\<Union>m<i. V m))) (h i)" for i
+ by (rule continuous_on_subset [OF conth]) auto
+ show "\<And>i j x. x \<in> {0..1} \<times> UNION UNIV V \<inter>
+ {0..1} \<times> (V i - (\<Union>m<i. V m)) \<inter> {0..1} \<times> (V j - (\<Union>m<j. V m))
+ \<Longrightarrow> h i x = h j x"
+ by clarsimp (metis lessThan_iff linorder_neqE_nat)
+ qed auto
+ show ?thesis
+ proof (simp add: homotopic_with eqU [symmetric], intro exI conjI ballI)
+ show "continuous_on ({0..1} \<times> \<Union>\<V>) \<zeta>"
+ using V eqU by (blast intro!: continuous_on_subset [OF cont])
+ show "\<zeta>` ({0..1} \<times> \<Union>\<V>) \<subseteq> T"
+ proof clarsimp
+ fix t :: real and y :: "'a" and X :: "'a set"
+ assume "y \<in> X" "X \<in> \<V>" and t: "0 \<le> t" "t \<le> 1"
+ then obtain k where "y \<in> V k" and j: "\<forall>j<k. y \<notin> V j"
+ by (metis image_iff V wop)
+ with him t show "\<zeta>(t, y) \<in> T"
+ by (subst eq) (force simp:)+
+ qed
+ fix X y
+ assume "X \<in> \<V>" "y \<in> X"
+ then obtain k where "y \<in> V k" and j: "\<forall>j<k. y \<notin> V j"
+ by (metis image_iff V wop)
+ then show "\<zeta>(0, y) = f y" and "\<zeta>(1, y) = g y"
+ by (subst eq [where i=k]; force simp: h0 h1)+
+ qed
+ qed
+qed
+
+proposition homotopic_on_components_eq:
+ fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set"
+ assumes S: "locally connected S \<or> compact S" and "ANR T"
+ shows "homotopic_with (\<lambda>x. True) S T f g \<longleftrightarrow>
+ (continuous_on S f \<and> f ` S \<subseteq> T \<and> continuous_on S g \<and> g ` S \<subseteq> T) \<and>
+ (\<forall>C \<in> components S. homotopic_with (\<lambda>x. True) C T f g)"
+ (is "?lhs \<longleftrightarrow> ?C \<and> ?rhs")
+proof -
+ have "continuous_on S f" "f ` S \<subseteq> T" "continuous_on S g" "g ` S \<subseteq> T" if ?lhs
+ using homotopic_with_imp_continuous homotopic_with_imp_subset1 homotopic_with_imp_subset2 that by blast+
+ moreover have "?lhs \<longleftrightarrow> ?rhs"
+ if contf: "continuous_on S f" and fim: "f ` S \<subseteq> T" and contg: "continuous_on S g" and gim: "g ` S \<subseteq> T"
+ proof
+ assume ?lhs
+ with that show ?rhs
+ by (simp add: homotopic_with_subset_left in_components_subset)
+ next
+ assume R: ?rhs
+ have "\<exists>U. C \<subseteq> U \<and> closedin (subtopology euclidean S) U \<and>
+ openin (subtopology euclidean S) U \<and>
+ homotopic_with (\<lambda>x. True) U T f g" if C: "C \<in> components S" for C
+ proof -
+ have "C \<subseteq> S"
+ by (simp add: in_components_subset that)
+ show ?thesis
+ using S
+ proof
+ assume "locally connected S"
+ show ?thesis
+ proof (intro exI conjI)
+ show "closedin (subtopology euclidean S) C"
+ by (simp add: closedin_component that)
+ show "openin (subtopology euclidean S) C"
+ by (simp add: \<open>locally connected S\<close> openin_components_locally_connected that)
+ show "homotopic_with (\<lambda>x. True) C T f g"
+ by (simp add: R that)
+ qed auto
+ next
+ assume "compact S"
+ have hom: "homotopic_with (\<lambda>x. True) C T f g"
+ using R that by blast
+ obtain U where "C \<subseteq> U" and opeU: "openin (subtopology euclidean S) U"
+ and hom: "homotopic_with (\<lambda>x. True) U T f g"
+ using homotopic_neighbourhood_extension [OF contf fim contg gim _ \<open>ANR T\<close> hom]
+ \<open>C \<in> components S\<close> closedin_component by blast
+ then obtain V where "open V" and V: "U = S \<inter> V"
+ by (auto simp: openin_open)
+ moreover have "locally compact S"
+ by (simp add: \<open>compact S\<close> closed_imp_locally_compact compact_imp_closed)
+ ultimately obtain K where opeK: "openin (subtopology euclidean S) K" and "compact K" "C \<subseteq> K" "K \<subseteq> V"
+ by (metis C Int_subset_iff Sura_Bura_clopen_subset \<open>C \<subseteq> U\<close> \<open>compact S\<close> compact_components)
+ show ?thesis
+ proof (intro exI conjI)
+ show "closedin (subtopology euclidean S) K"
+ by (meson \<open>compact K\<close> \<open>compact S\<close> closedin_compact_eq opeK openin_imp_subset)
+ show "homotopic_with (\<lambda>x. True) K T f g"
+ using V \<open>K \<subseteq> V\<close> hom homotopic_with_subset_left opeK openin_imp_subset by fastforce
+ qed (use opeK \<open>C \<subseteq> K\<close> in auto)
+ qed
+ qed
+ then obtain \<phi> where \<phi>: "\<And>C. C \<in> components S \<Longrightarrow> C \<subseteq> \<phi> C"
+ and clo\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> closedin (subtopology euclidean S) (\<phi> C)"
+ and ope\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> openin (subtopology euclidean S) (\<phi> C)"
+ and hom\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> homotopic_with (\<lambda>x. True) (\<phi> C) T f g"
+ by metis
+ have Seq: "S = UNION (components S) \<phi>"
+ proof
+ show "S \<subseteq> UNION (components S) \<phi>"
+ by (metis Sup_mono Union_components \<phi> imageI)
+ show "UNION (components S) \<phi> \<subseteq> S"
+ using ope\<phi> openin_imp_subset by fastforce
+ qed
+ show ?lhs
+ apply (subst Seq)
+ apply (rule homotopic_on_clopen_Union)
+ using Seq clo\<phi> ope\<phi> hom\<phi> by auto
+ qed
+ ultimately show ?thesis by blast
+qed
+
+
+lemma cohomotopically_trivial_on_components:
+ fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set"
+ assumes S: "locally connected S \<or> compact S" and "ANR T"
+ shows
+ "(\<forall>f g. continuous_on S f \<longrightarrow> f ` S \<subseteq> T \<longrightarrow> continuous_on S g \<longrightarrow> g ` S \<subseteq> T \<longrightarrow>
+ homotopic_with (\<lambda>x. True) S T f g)
+ \<longleftrightarrow>
+ (\<forall>C\<in>components S.
+ \<forall>f g. continuous_on C f \<longrightarrow> f ` C \<subseteq> T \<longrightarrow> continuous_on C g \<longrightarrow> g ` C \<subseteq> T \<longrightarrow>
+ homotopic_with (\<lambda>x. True) C T f g)"
+ (is "?lhs = ?rhs")
+proof
+ assume L[rule_format]: ?lhs
+ show ?rhs
+ proof clarify
+ fix C f g
+ assume contf: "continuous_on C f" and fim: "f ` C \<subseteq> T"
+ and contg: "continuous_on C g" and gim: "g ` C \<subseteq> T" and C: "C \<in> components S"
+ obtain f' where contf': "continuous_on S f'" and f'im: "f' ` S \<subseteq> T" and f'f: "\<And>x. x \<in> C \<Longrightarrow> f' x = f x"
+ using extension_from_component [OF S \<open>ANR T\<close> C contf fim] by metis
+ obtain g' where contg': "continuous_on S g'" and g'im: "g' ` S \<subseteq> T" and g'g: "\<And>x. x \<in> C \<Longrightarrow> g' x = g x"
+ using extension_from_component [OF S \<open>ANR T\<close> C contg gim] by metis
+ have "homotopic_with (\<lambda>x. True) C T f' g'"
+ using L [OF contf' f'im contg' g'im] homotopic_with_subset_left C in_components_subset by fastforce
+ then show "homotopic_with (\<lambda>x. True) C T f g"
+ using f'f g'g homotopic_with_eq by force
+ qed
+next
+ assume R [rule_format]: ?rhs
+ show ?lhs
+ proof clarify
+ fix f g
+ assume contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
+ and contg: "continuous_on S g" and gim: "g ` S \<subseteq> T"
+ moreover have "homotopic_with (\<lambda>x. True) C T f g" if "C \<in> components S" for C
+ using R [OF that]
+ by (meson contf contg continuous_on_subset fim gim image_mono in_components_subset order.trans that)
+ ultimately show "homotopic_with (\<lambda>x. True) S T f g"
+ by (subst homotopic_on_components_eq [OF S \<open>ANR T\<close>]) auto
+ qed
+qed
+
+
subsection\<open>The complement of a set and path-connectedness\<close>
text\<open>Complement in dimension N > 1 of set homeomorphic to any interval in
diff -r d0f12783cd80 -r 04678058308f src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy Sun Oct 29 19:39:03 2017 +0100
+++ b/src/HOL/Analysis/Connected.thy Mon Oct 30 16:02:59 2017 +0000
@@ -810,6 +810,10 @@
by (auto simp: closedin_closed)
qed
+lemma closedin_component:
+ "C \<in> components s \<Longrightarrow> closedin (subtopology euclidean s) C"
+ using closedin_connected_component componentsE by blast
+
subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
@@ -3235,39 +3239,29 @@
using assms
by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified])
-text\<open>Some more convenient intermediate-value theorem formulations.\<close>
+subsubsection\<open>Some more convenient intermediate-value theorem formulations.\<close>
lemma connected_ivt_hyperplane:
- assumes "connected s"
- and "x \<in> s"
- and "y \<in> s"
- and "inner a x \<le> b"
- and "b \<le> inner a y"
- shows "\<exists>z \<in> s. inner a z = b"
+ assumes "connected S" and xy: "x \<in> S" "y \<in> S" and b: "inner a x \<le> b" "b \<le> inner a y"
+ shows "\<exists>z \<in> S. inner a z = b"
proof (rule ccontr)
- assume as:"\<not> (\<exists>z\<in>s. inner a z = b)"
+ assume as:"\<not> (\<exists>z\<in>S. inner a z = b)"
let ?A = "{x. inner a x < b}"
let ?B = "{x. inner a x > b}"
have "open ?A" "open ?B"
using open_halfspace_lt and open_halfspace_gt by auto
- moreover
- have "?A \<inter> ?B = {}" by auto
- moreover
- have "s \<subseteq> ?A \<union> ?B" using as by auto
- ultimately
- show False
- using assms(1)[unfolded connected_def not_ex,
+ moreover have "?A \<inter> ?B = {}" by auto
+ moreover have "S \<subseteq> ?A \<union> ?B" using as by auto
+ ultimately show False
+ using \<open>connected S\<close>[unfolded connected_def not_ex,
THEN spec[where x="?A"], THEN spec[where x="?B"]]
- using assms(2-5)
- by auto
+ using xy b by auto
qed
lemma connected_ivt_component:
fixes x::"'a::euclidean_space"
- shows "connected s \<Longrightarrow>
- x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow>
- x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>s. z\<bullet>k = a)"
- using connected_ivt_hyperplane[of s x y "k::'a" a]
+ shows "connected S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>S. z\<bullet>k = a)"
+ using connected_ivt_hyperplane[of S x y "k::'a" a]
by (auto simp: inner_commute)
lemma image_affinity_cbox: fixes m::real
@@ -4942,7 +4936,7 @@
qed
-proposition component_complement_connected:
+proposition component_diff_connected:
fixes S :: "'a::metric_space set"
assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
shows "connected(U - C)"
diff -r d0f12783cd80 -r 04678058308f src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Oct 29 19:39:03 2017 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Oct 30 16:02:59 2017 +0000
@@ -2373,7 +2373,14 @@
qed
corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
- by(simp add: convex_connected)
+ by (simp add: convex_connected)
+
+corollary component_complement_connected:
+ fixes S :: "'a::real_normed_vector set"
+ assumes "connected S" "C \<in> components (-S)"
+ shows "connected(-C)"
+ using component_diff_connected [of S UNIV] assms
+ by (auto simp: Compl_eq_Diff_UNIV)
proposition clopen:
fixes S :: "'a :: real_normed_vector set"
diff -r d0f12783cd80 -r 04678058308f src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy Sun Oct 29 19:39:03 2017 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Mon Oct 30 16:02:59 2017 +0000
@@ -4589,4 +4589,788 @@
using fk gfh kTS by force
qed
+
+text\<open>If two points are separated by a closed set, there's a minimal one.\<close>
+proposition closed_irreducible_separator:
+ fixes a :: "'a::real_normed_vector"
+ assumes "closed S" and ab: "\<not> connected_component (- S) a b"
+ obtains T where "T \<subseteq> S" "closed T" "T \<noteq> {}" "\<not> connected_component (- T) a b"
+ "\<And>U. U \<subset> T \<Longrightarrow> connected_component (- U) a b"
+proof (cases "a \<in> S \<or> b \<in> S")
+ case True
+ then show ?thesis
+ proof
+ assume *: "a \<in> S"
+ show ?thesis
+ proof
+ show "{a} \<subseteq> S"
+ using * by blast
+ show "\<not> connected_component (- {a}) a b"
+ using connected_component_in by auto
+ show "\<And>U. U \<subset> {a} \<Longrightarrow> connected_component (- U) a b"
+ by (metis connected_component_UNIV UNIV_I compl_bot_eq connected_component_eq_eq less_le_not_le subset_singletonD)
+ qed auto
+ next
+ assume *: "b \<in> S"
+ show ?thesis
+ proof
+ show "{b} \<subseteq> S"
+ using * by blast
+ show "\<not> connected_component (- {b}) a b"
+ using connected_component_in by auto
+ show "\<And>U. U \<subset> {b} \<Longrightarrow> connected_component (- U) a b"
+ by (metis connected_component_UNIV UNIV_I compl_bot_eq connected_component_eq_eq less_le_not_le subset_singletonD)
+ qed auto
+ qed
+next
+ case False
+ define A where "A \<equiv> connected_component_set (- S) a"
+ define B where "B \<equiv> connected_component_set (- (closure A)) b"
+ have "a \<in> A"
+ using False A_def by auto
+ have "b \<in> B"
+ unfolding A_def B_def closure_Un_frontier
+ using ab False \<open>closed S\<close> frontier_complement frontier_of_connected_component_subset frontier_subset_closed by force
+ have "frontier B \<subseteq> frontier (connected_component_set (- closure A) b)"
+ using B_def by blast
+ also have frsub: "... \<subseteq> frontier A"
+ proof -
+ have "\<And>A. closure (- closure (- A)) \<subseteq> closure A"
+ by (metis (no_types) closure_mono closure_subset compl_le_compl_iff double_compl)
+ then show ?thesis
+ by (metis (no_types) closure_closure double_compl frontier_closures frontier_of_connected_component_subset le_inf_iff subset_trans)
+ qed
+ finally have frBA: "frontier B \<subseteq> frontier A" .
+ show ?thesis
+ proof
+ show "frontier B \<subseteq> S"
+ proof -
+ have "frontier S \<subseteq> S"
+ by (simp add: \<open>closed S\<close> frontier_subset_closed)
+ then show ?thesis
+ using frsub frontier_complement frontier_of_connected_component_subset
+ unfolding A_def B_def by blast
+ qed
+ show "closed (frontier B)"
+ by simp
+ show "\<not> connected_component (- frontier B) a b"
+ unfolding connected_component_def
+ proof clarify
+ fix T
+ assume "connected T" and TB: "T \<subseteq> - frontier B" and "a \<in> T" and "b \<in> T"
+ have "a \<notin> B"
+ 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)
+ have "T \<inter> B \<noteq> {}"
+ using \<open>b \<in> B\<close> \<open>b \<in> T\<close> by blast
+ moreover have "T - B \<noteq> {}"
+ using \<open>a \<notin> B\<close> \<open>a \<in> T\<close> by blast
+ ultimately show "False"
+ using connected_Int_frontier [of T B] TB \<open>connected T\<close> by blast
+ qed
+ moreover have "connected_component (- frontier B) a b" if "frontier B = {}"
+ apply (simp add: that)
+ using connected_component_eq_UNIV by blast
+ ultimately show "frontier B \<noteq> {}"
+ by blast
+ show "connected_component (- U) a b" if "U \<subset> frontier B" for U
+ proof -
+ obtain p where Usub: "U \<subseteq> frontier B" and p: "p \<in> frontier B" "p \<notin> U"
+ using \<open>U \<subset> frontier B\<close> by blast
+ show ?thesis
+ unfolding connected_component_def
+ proof (intro exI conjI)
+ have "connected ((insert p A) \<union> (insert p B))"
+ proof (rule connected_Un)
+ show "connected (insert p A)"
+ 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)
+ show "connected (insert p B)"
+ 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)
+ qed blast
+ then show "connected (insert p (B \<union> A))"
+ by (simp add: sup.commute)
+ have "A \<subseteq> - U"
+ using A_def Usub \<open>frontier B \<subseteq> S\<close> connected_component_subset by fastforce
+ moreover have "B \<subseteq> - U"
+ using B_def Usub connected_component_subset frBA frontier_closures by fastforce
+ ultimately show "insert p (B \<union> A) \<subseteq> - U"
+ using p by auto
+ qed (auto simp: \<open>a \<in> A\<close> \<open>b \<in> B\<close>)
+ qed
+ qed
+qed
+
+lemma frontier_minimal_separating_closed_pointwise:
+ fixes S :: "'a::real_normed_vector set"
+ assumes S: "closed S" "a \<notin> S" and nconn: "\<not> connected_component (- S) a b"
+ and conn: "\<And>T. \<lbrakk>closed T; T \<subset> S\<rbrakk> \<Longrightarrow> connected_component (- T) a b"
+ shows "frontier(connected_component_set (- S) a) = S" (is "?F = S")
+proof -
+ have "?F \<subseteq> S"
+ by (simp add: S componentsI frontier_of_components_closed_complement)
+ moreover have False if "?F \<subset> S"
+ proof -
+ have "connected_component (- ?F) a b"
+ by (simp add: conn that)
+ then obtain T where "connected T" "T \<subseteq> -?F" "a \<in> T" "b \<in> T"
+ by (auto simp: connected_component_def)
+ moreover have "T \<inter> ?F \<noteq> {}"
+ proof (rule connected_Int_frontier [OF \<open>connected T\<close>])
+ show "T \<inter> connected_component_set (- S) a \<noteq> {}"
+ using \<open>a \<notin> S\<close> \<open>a \<in> T\<close> by fastforce
+ show "T - connected_component_set (- S) a \<noteq> {}"
+ using \<open>b \<in> T\<close> nconn by blast
+ qed
+ ultimately show ?thesis
+ by blast
+ qed
+ ultimately show ?thesis
+ by blast
+qed
+
+
+subsection\<open>Unicoherence (closed)\<close>
+
+definition unicoherent where
+ "unicoherent U \<equiv>
+ \<forall>S T. connected S \<and> connected T \<and> S \<union> T = U \<and>
+ closedin (subtopology euclidean U) S \<and> closedin (subtopology euclidean U) T
+ \<longrightarrow> connected (S \<inter> T)"
+
+lemma unicoherentI [intro?]:
+ assumes "\<And>S T. \<lbrakk>connected S; connected T; U = S \<union> T; closedin (subtopology euclidean U) S; closedin (subtopology euclidean U) T\<rbrakk>
+ \<Longrightarrow> connected (S \<inter> T)"
+ shows "unicoherent U"
+ using assms unfolding unicoherent_def by blast
+
+lemma unicoherentD:
+ assumes "unicoherent U" "connected S" "connected T" "U = S \<union> T" "closedin (subtopology euclidean U) S" "closedin (subtopology euclidean U) T"
+ shows "connected (S \<inter> T)"
+ using assms unfolding unicoherent_def by blast
+
+lemma homeomorphic_unicoherent:
+ assumes ST: "S homeomorphic T" and S: "unicoherent S"
+ shows "unicoherent T"
+proof -
+ 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"
+ and contf: "continuous_on S f" and contg: "continuous_on (f ` S) g"
+ using ST by (auto simp: homeomorphic_def homeomorphism_def)
+ show ?thesis
+ proof
+ fix U V
+ assume "connected U" "connected V" and T: "T = U \<union> V"
+ and cloU: "closedin (subtopology euclidean T) U"
+ and cloV: "closedin (subtopology euclidean T) V"
+ have "f ` (g ` U \<inter> g ` V) \<subseteq> U" "f ` (g ` U \<inter> g ` V) \<subseteq> V"
+ using gf fim T by auto (metis UnCI image_iff)+
+ moreover have "U \<inter> V \<subseteq> f ` (g ` U \<inter> g ` V)"
+ using gf fim by (force simp: image_iff T)
+ ultimately have "U \<inter> V = f ` (g ` U \<inter> g ` V)" by blast
+ moreover have "connected (f ` (g ` U \<inter> g ` V))"
+ proof (rule connected_continuous_image)
+ show "continuous_on (g ` U \<inter> g ` V) f"
+ apply (rule continuous_on_subset [OF contf])
+ using T fim gfim by blast
+ show "connected (g ` U \<inter> g ` V)"
+ proof (intro conjI unicoherentD [OF S])
+ show "connected (g ` U)" "connected (g ` V)"
+ using \<open>connected U\<close> cloU \<open>connected V\<close> cloV
+ by (metis Topological_Spaces.connected_continuous_image closedin_imp_subset contg continuous_on_subset fim)+
+ show "S = g ` U \<union> g ` V"
+ using T fim gfim by auto
+ have hom: "homeomorphism T S g f"
+ by (simp add: contf contg fim gf gfim homeomorphism_def)
+ have "closedin (subtopology euclidean T) U" "closedin (subtopology euclidean T) V"
+ by (simp_all add: cloU cloV)
+ then show "closedin (subtopology euclidean S) (g ` U)"
+ "closedin (subtopology euclidean S) (g ` V)"
+ by (blast intro: homeomorphism_imp_closed_map [OF hom])+
+ qed
+ qed
+ ultimately show "connected (U \<inter> V)" by metis
+ qed
+qed
+
+
+lemma homeomorphic_unicoherent_eq:
+ "S homeomorphic T \<Longrightarrow> (unicoherent S \<longleftrightarrow> unicoherent T)"
+ by (meson homeomorphic_sym homeomorphic_unicoherent)
+
+lemma unicoherent_translation:
+ fixes S :: "'a::real_normed_vector set"
+ shows
+ "unicoherent (image (\<lambda>x. a + x) S) \<longleftrightarrow> unicoherent S"
+ using homeomorphic_translation homeomorphic_unicoherent_eq by blast
+
+lemma unicoherent_injective_linear_image:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "linear f" "inj f"
+ shows "(unicoherent(f ` S) \<longleftrightarrow> unicoherent S)"
+ using assms homeomorphic_unicoherent_eq linear_homeomorphic_image by blast
+
+
+lemma Borsukian_imp_unicoherent:
+ fixes U :: "'a::euclidean_space set"
+ assumes "Borsukian U" shows "unicoherent U"
+ unfolding unicoherent_def
+proof clarify
+ fix S T
+ assume "connected S" "connected T" "U = S \<union> T"
+ and cloS: "closedin (subtopology euclidean (S \<union> T)) S"
+ and cloT: "closedin (subtopology euclidean (S \<union> T)) T"
+ show "connected (S \<inter> T)"
+ unfolding connected_closedin_eq
+ proof clarify
+ fix V W
+ assume "closedin (subtopology euclidean (S \<inter> T)) V"
+ and "closedin (subtopology euclidean (S \<inter> T)) W"
+ and VW: "V \<union> W = S \<inter> T" "V \<inter> W = {}" and "V \<noteq> {}" "W \<noteq> {}"
+ then have cloV: "closedin (subtopology euclidean U) V" and cloW: "closedin (subtopology euclidean U) W"
+ using \<open>U = S \<union> T\<close> cloS cloT closedin_trans by blast+
+ obtain q where contq: "continuous_on U q"
+ and q01: "\<And>x. x \<in> U \<Longrightarrow> q x \<in> {0..1::real}"
+ and qV: "\<And>x. x \<in> V \<Longrightarrow> q x = 0" and qW: "\<And>x. x \<in> W \<Longrightarrow> q x = 1"
+ by (rule Urysohn_local [OF cloV cloW \<open>V \<inter> W = {}\<close>, of 0 1])
+ (fastforce simp: closed_segment_eq_real_ivl)
+ let ?h = "\<lambda>x. if x \<in> S then exp(pi * \<i> * q x) else 1 / exp(pi * \<i> * q x)"
+ have eqST: "exp(pi * \<i> * q x) = 1 / exp(pi * \<i> * q x)" if "x \<in> S \<inter> T" for x
+ proof -
+ have "x \<in> V \<union> W"
+ using that \<open>V \<union> W = S \<inter> T\<close> by blast
+ with qV qW show ?thesis by force
+ qed
+ obtain g where contg: "continuous_on U g"
+ and circle: "g ` U \<subseteq> sphere 0 1"
+ and S: "\<And>x. x \<in> S \<Longrightarrow> g x = exp(pi * \<i> * q x)"
+ and T: "\<And>x. x \<in> T \<Longrightarrow> g x = 1 / exp(pi * \<i> * q x)"
+ proof
+ show "continuous_on U ?h"
+ unfolding \<open>U = S \<union> T\<close>
+ proof (rule continuous_on_cases_local [OF cloS cloT])
+ show "continuous_on S (\<lambda>x. exp (pi * \<i> * q x))"
+ apply (intro continuous_intros)
+ using \<open>U = S \<union> T\<close> continuous_on_subset contq by blast
+ show "continuous_on T (\<lambda>x. 1 / exp (pi * \<i> * q x))"
+ apply (intro continuous_intros)
+ using \<open>U = S \<union> T\<close> continuous_on_subset contq by auto
+ qed (use eqST in auto)
+ qed (use eqST in \<open>auto simp: norm_divide\<close>)
+ then obtain h where conth: "continuous_on U h" and heq: "\<And>x. x \<in> U \<Longrightarrow> g x = exp (h x)"
+ by (metis Borsukian_continuous_logarithm_circle assms)
+ obtain v w where "v \<in> V" "w \<in> W"
+ using \<open>V \<noteq> {}\<close> \<open>W \<noteq> {}\<close> by blast
+ then have vw: "v \<in> S \<inter> T" "w \<in> S \<inter> T"
+ using VW by auto
+ have iff: "2 * pi \<le> cmod (2 * of_int m * of_real pi * \<i> - 2 * of_int n * of_real pi * \<i>)
+ \<longleftrightarrow> 1 \<le> abs (m - n)" for m n
+ proof -
+ have "2 * pi \<le> cmod (2 * of_int m * of_real pi * \<i> - 2 * of_int n * of_real pi * \<i>)
+ \<longleftrightarrow> 2 * pi \<le> cmod ((2 * pi * \<i>) * (of_int m - of_int n))"
+ by (simp add: algebra_simps)
+ also have "... \<longleftrightarrow> 2 * pi \<le> 2 * pi * cmod (of_int m - of_int n)"
+ by (simp add: norm_mult)
+ also have "... \<longleftrightarrow> 1 \<le> abs (m - n)"
+ by simp (metis norm_of_int of_int_1_le_iff of_int_abs of_int_diff)
+ finally show ?thesis .
+ qed
+ have *: "\<exists>n::int. h x - (pi * \<i> * q x) = (of_int(2*n) * pi) * \<i>" if "x \<in> S" for x
+ using that S \<open>U = S \<union> T\<close> heq exp_eq [symmetric] by (simp add: algebra_simps)
+ moreover have "(\<lambda>x. h x - (pi * \<i> * q x)) constant_on S"
+ proof (rule continuous_discrete_range_constant [OF \<open>connected S\<close>])
+ have "continuous_on S h" "continuous_on S q"
+ using \<open>U = S \<union> T\<close> continuous_on_subset conth contq by blast+
+ then show "continuous_on S (\<lambda>x. h x - (pi * \<i> * q x))"
+ by (intro continuous_intros)
+ have "2*pi \<le> cmod (h y - (pi * \<i> * q y) - (h x - (pi * \<i> * q x)))"
+ 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
+ using * [OF \<open>x \<in> S\<close>] * [OF \<open>y \<in> S\<close>] ne by (auto simp: iff)
+ then show "\<And>x. x \<in> S \<Longrightarrow>
+ \<exists>e>0. \<forall>y. y \<in> S \<and> h y - (pi * \<i> * q y) \<noteq> h x - (pi * \<i> * q x) \<longrightarrow>
+ e \<le> cmod (h y - (pi * \<i> * q y) - (h x - (pi * \<i> * q x)))"
+ by (rule_tac x="2*pi" in exI) auto
+ qed
+ ultimately
+ obtain m where m: "\<And>x. x \<in> S \<Longrightarrow> h x - (pi * \<i> * q x) = (of_int(2*m) * pi) * \<i>"
+ using vw by (force simp: constant_on_def)
+ have *: "\<exists>n::int. h x = - (pi * \<i> * q x) + (of_int(2*n) * pi) * \<i>" if "x \<in> T" for x
+ unfolding exp_eq [symmetric]
+ using that T \<open>U = S \<union> T\<close> by (simp add: exp_minus field_simps heq [symmetric])
+ moreover have "(\<lambda>x. h x + (pi * \<i> * q x)) constant_on T"
+ proof (rule continuous_discrete_range_constant [OF \<open>connected T\<close>])
+ have "continuous_on T h" "continuous_on T q"
+ using \<open>U = S \<union> T\<close> continuous_on_subset conth contq by blast+
+ then show "continuous_on T (\<lambda>x. h x + (pi * \<i> * q x))"
+ by (intro continuous_intros)
+ have "2*pi \<le> cmod (h y + (pi * \<i> * q y) - (h x + (pi * \<i> * q x)))"
+ 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
+ using * [OF \<open>x \<in> T\<close>] * [OF \<open>y \<in> T\<close>] ne by (auto simp: iff)
+ then show "\<And>x. x \<in> T \<Longrightarrow>
+ \<exists>e>0. \<forall>y. y \<in> T \<and> h y + (pi * \<i> * q y) \<noteq> h x + (pi * \<i> * q x) \<longrightarrow>
+ e \<le> cmod (h y + (pi * \<i> * q y) - (h x + (pi * \<i> * q x)))"
+ by (rule_tac x="2*pi" in exI) auto
+ qed
+ ultimately
+ obtain n where n: "\<And>x. x \<in> T \<Longrightarrow> h x + (pi * \<i> * q x) = (of_int(2*n) * pi) * \<i>"
+ using vw by (force simp: constant_on_def)
+ show "False"
+ using m [of v] m [of w] n [of v] n [of w] vw
+ by (auto simp: algebra_simps \<open>v \<in> V\<close> \<open>w \<in> W\<close> qV qW)
+ qed
+qed
+
+
+corollary contractible_imp_unicoherent:
+ fixes U :: "'a::euclidean_space set"
+ assumes "contractible U" shows "unicoherent U"
+ by (simp add: Borsukian_imp_unicoherent assms contractible_imp_Borsukian)
+
+corollary convex_imp_unicoherent:
+ fixes U :: "'a::euclidean_space set"
+ assumes "convex U" shows "unicoherent U"
+ by (simp add: Borsukian_imp_unicoherent assms convex_imp_Borsukian)
+
+text\<open>If the type class constraint can be relaxed, I don't know how!\<close>
+corollary unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)"
+ by (simp add: convex_imp_unicoherent)
+
+
+lemma unicoherent_monotone_image_compact:
+ fixes T :: "'b :: t2_space set"
+ assumes S: "unicoherent S" "compact S" and contf: "continuous_on S f" and fim: "f ` S = T"
+ and conn: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
+ shows "unicoherent T"
+proof
+ fix U V
+ assume UV: "connected U" "connected V" "T = U \<union> V"
+ and cloU: "closedin (subtopology euclidean T) U"
+ and cloV: "closedin (subtopology euclidean T) V"
+ moreover have "compact T"
+ using \<open>compact S\<close> compact_continuous_image contf fim by blast
+ ultimately have "closed U" "closed V"
+ by (auto simp: closedin_closed_eq compact_imp_closed)
+ let ?SUV = "(S \<inter> f -` U) \<inter> (S \<inter> f -` V)"
+ have UV_eq: "f ` ?SUV = U \<inter> V"
+ using \<open>T = U \<union> V\<close> fim by force+
+ have "connected (f ` ?SUV)"
+ proof (rule connected_continuous_image)
+ show "continuous_on ?SUV f"
+ by (meson contf continuous_on_subset inf_le1)
+ show "connected ?SUV"
+ proof (rule unicoherentD [OF \<open>unicoherent S\<close>, of "S \<inter> f -` U" "S \<inter> f -` V"])
+ have "\<And>C. closedin (subtopology euclidean S) C \<Longrightarrow> closedin (subtopology euclidean T) (f ` C)"
+ 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)
+ then show "connected (S \<inter> f -` U)" "connected (S \<inter> f -` V)"
+ using UV by (auto simp: conn intro: connected_closed_monotone_preimage [OF contf fim])
+ show "S = (S \<inter> f -` U) \<union> (S \<inter> f -` V)"
+ using UV fim by blast
+ show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
+ "closedin (subtopology euclidean S) (S \<inter> f -` V)"
+ by (auto simp: continuous_on_imp_closedin cloU cloV contf fim)
+ qed
+ qed
+ with UV_eq show "connected (U \<inter> V)"
+ by simp
+qed
+
+
+
+subsection\<open>Several common variants of unicoherence\<close>
+
+lemma connected_frontier_simple:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "connected S" "connected(- S)" shows "connected(frontier S)"
+ unfolding frontier_closures
+ apply (rule unicoherentD [OF unicoherent_UNIV])
+ apply (simp_all add: assms connected_imp_connected_closure)
+ by (simp add: closure_def)
+
+lemma connected_frontier_component_complement:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "connected S" and C: "C \<in> components(- S)" shows "connected(frontier C)"
+ apply (rule connected_frontier_simple)
+ using C in_components_connected apply blast
+ by (metis Compl_eq_Diff_UNIV connected_UNIV assms top_greatest component_complement_connected)
+
+lemma connected_frontier_disjoint:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "connected S" "connected T" "disjnt S T" and ST: "frontier S \<subseteq> frontier T"
+ shows "connected(frontier S)"
+proof (cases "S = UNIV")
+ case True then show ?thesis
+ by simp
+next
+ case False
+ then have "-S \<noteq> {}"
+ by blast
+ then obtain C where C: "C \<in> components(- S)" and "T \<subseteq> C"
+ by (metis ComplI disjnt_iff subsetI exists_component_superset \<open>disjnt S T\<close> \<open>connected T\<close>)
+ moreover have "frontier S = frontier C"
+ proof -
+ have "frontier C \<subseteq> frontier S"
+ using C frontier_complement frontier_of_components_subset by blast
+ moreover have "x \<in> frontier C" if "x \<in> frontier S" for x
+ proof -
+ have "x \<in> closure C"
+ using that unfolding frontier_def
+ by (metis (no_types) Diff_eq ST \<open>T \<subseteq> C\<close> closure_mono contra_subsetD frontier_def le_inf_iff that)
+ moreover have "x \<notin> interior C"
+ using that unfolding frontier_def
+ by (metis C Compl_eq_Diff_UNIV Diff_iff subsetD in_components_subset interior_diff interior_mono)
+ ultimately show ?thesis
+ by (auto simp: frontier_def)
+ qed
+ ultimately show ?thesis
+ by blast
+ qed
+ ultimately show ?thesis
+ using \<open>connected S\<close> connected_frontier_component_complement by auto
+qed
+
+lemma separation_by_component_closed_pointwise:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "closed S" "\<not> connected_component (- S) a b"
+ obtains C where "C \<in> components S" "\<not> connected_component(- C) a b"
+proof (cases "a \<in> S \<or> b \<in> S")
+ case True
+ then show ?thesis
+ using connected_component_in componentsI that by fastforce
+next
+ case False
+ obtain T where "T \<subseteq> S" "closed T" "T \<noteq> {}"
+ and nab: "\<not> connected_component (- T) a b"
+ and conn: "\<And>U. U \<subset> T \<Longrightarrow> connected_component (- U) a b"
+ using closed_irreducible_separator [OF assms] by metis
+ moreover have "connected T"
+ proof -
+ have ab: "frontier(connected_component_set (- T) a) = T" "frontier(connected_component_set (- T) b) = T"
+ using frontier_minimal_separating_closed_pointwise
+ 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)+
+ have "connected (frontier (connected_component_set (- T) a))"
+ proof (rule connected_frontier_disjoint)
+ show "disjnt (connected_component_set (- T) a) (connected_component_set (- T) b)"
+ unfolding disjnt_iff
+ by (metis connected_component_eq connected_component_eq_empty connected_component_idemp mem_Collect_eq nab)
+ show "frontier (connected_component_set (- T) a) \<subseteq> frontier (connected_component_set (- T) b)"
+ by (simp add: ab)
+ qed auto
+ with ab \<open>closed T\<close> show ?thesis
+ by simp
+ qed
+ ultimately obtain C where "C \<in> components S" "T \<subseteq> C"
+ using exists_component_superset [of T S] by blast
+ then show ?thesis
+ by (meson Compl_anti_mono connected_component_of_subset nab that)
+qed
+
+
+lemma separation_by_component_closed:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "closed S" "\<not> connected(- S)"
+ obtains C where "C \<in> components S" "\<not> connected(- C)"
+proof -
+ obtain x y where "closed S" "x \<notin> S" "y \<notin> S" and "\<not> connected_component (- S) x y"
+ using assms by (auto simp: connected_iff_connected_component)
+ then obtain C where "C \<in> components S" "\<not> connected_component(- C) x y"
+ using separation_by_component_closed_pointwise by metis
+ then show "thesis"
+ apply (clarify elim!: componentsE)
+ 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)
+qed
+
+lemma separation_by_Un_closed_pointwise:
+ fixes S :: "'a :: euclidean_space set"
+ assumes ST: "closed S" "closed T" "S \<inter> T = {}"
+ and conS: "connected_component (- S) a b" and conT: "connected_component (- T) a b"
+ shows "connected_component (- (S \<union> T)) a b"
+proof (rule ccontr)
+ have "a \<notin> S" "b \<notin> S" "a \<notin> T" "b \<notin> T"
+ using conS conT connected_component_in by auto
+ assume "\<not> connected_component (- (S \<union> T)) a b"
+ then obtain C where "C \<in> components (S \<union> T)" and C: "\<not> connected_component(- C) a b"
+ using separation_by_component_closed_pointwise assms by blast
+ then have "C \<subseteq> S \<or> C \<subseteq> T"
+ proof -
+ have "connected C" "C \<subseteq> S \<union> T"
+ using \<open>C \<in> components (S \<union> T)\<close> in_components_subset by (blast elim: componentsE)+
+ moreover then have "C \<inter> T = {} \<or> C \<inter> S = {}"
+ by (metis Int_empty_right ST inf.commute connected_closed)
+ ultimately show ?thesis
+ by blast
+ qed
+ then show False
+ by (meson Compl_anti_mono C conS conT connected_component_of_subset)
+qed
+
+lemma separation_by_Un_closed:
+ fixes S :: "'a :: euclidean_space set"
+ assumes ST: "closed S" "closed T" "S \<inter> T = {}" and conS: "connected(- S)" and conT: "connected(- T)"
+ shows "connected(- (S \<union> T))"
+ using assms separation_by_Un_closed_pointwise
+ by (fastforce simp add: connected_iff_connected_component)
+
+lemma open_unicoherent_UNIV:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "open S" "open T" "connected S" "connected T" "S \<union> T = UNIV"
+ shows "connected(S \<inter> T)"
+proof -
+ have "connected(- (-S \<union> -T))"
+ by (metis closed_Compl compl_sup compl_top_eq double_compl separation_by_Un_closed assms)
+ then show ?thesis
+ by simp
+qed
+
+lemma separation_by_component_open_aux:
+ fixes S :: "'a :: euclidean_space set"
+ assumes ST: "closed S" "closed T" "S \<inter> T = {}"
+ and "S \<noteq> {}" "T \<noteq> {}"
+ obtains C where "C \<in> components(-(S \<union> T))" "C \<noteq> {}" "frontier C \<inter> S \<noteq> {}" "frontier C \<inter> T \<noteq> {}"
+proof (rule ccontr)
+ let ?S = "S \<union> \<Union>{C \<in> components(- (S \<union> T)). frontier C \<subseteq> S}"
+ let ?T = "T \<union> \<Union>{C \<in> components(- (S \<union> T)). frontier C \<subseteq> T}"
+ assume "~ thesis"
+ with that have *: "frontier C \<inter> S = {} \<or> frontier C \<inter> T = {}"
+ if C: "C \<in> components (- (S \<union> T))" "C \<noteq> {}" for C
+ using C by blast
+ 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> {}"
+ proof (intro exI conjI)
+ have "frontier (\<Union>{C \<in> components (- S \<inter> - T). frontier C \<subseteq> S}) \<subseteq> S"
+ apply (rule subset_trans [OF frontier_Union_subset_closure])
+ by (metis (no_types, lifting) SUP_least \<open>closed S\<close> closure_minimal mem_Collect_eq)
+ then have "frontier ?S \<subseteq> S"
+ by (simp add: frontier_subset_eq assms subset_trans [OF frontier_Un_subset])
+ then show "closed ?S"
+ using frontier_subset_eq by fastforce
+ have "frontier (\<Union>{C \<in> components (- S \<inter> - T). frontier C \<subseteq> T}) \<subseteq> T"
+ apply (rule subset_trans [OF frontier_Union_subset_closure])
+ by (metis (no_types, lifting) SUP_least \<open>closed T\<close> closure_minimal mem_Collect_eq)
+ then have "frontier ?T \<subseteq> T"
+ by (simp add: frontier_subset_eq assms subset_trans [OF frontier_Un_subset])
+ then show "closed ?T"
+ using frontier_subset_eq by fastforce
+ have "UNIV \<subseteq> (S \<union> T) \<union> \<Union>(components(- (S \<union> T)))"
+ using Union_components by blast
+ also have "... \<subseteq> ?S \<union> ?T"
+ proof -
+ have "C \<in> components (-(S \<union> T)) \<and> frontier C \<subseteq> S \<or>
+ C \<in> components (-(S \<union> T)) \<and> frontier C \<subseteq> T"
+ if "C \<in> components (- (S \<union> T))" "C \<noteq> {}" for C
+ using * [OF that] that
+ 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)
+ then show ?thesis
+ by blast
+ qed
+ finally show "UNIV \<subseteq> ?S \<union> ?T" .
+ have "\<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> S} \<union>
+ \<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> T} \<subseteq> - (S \<union> T)"
+ using in_components_subset by fastforce
+ moreover have "\<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> S} \<inter>
+ \<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> T} = {}"
+ proof -
+ have "C \<inter> C' = {}" if "C \<in> components (- (S \<union> T))" "frontier C \<subseteq> S"
+ "C' \<in> components (- (S \<union> T))" "frontier C' \<subseteq> T" for C C'
+ proof -
+ have NUN: "- S \<inter> - T \<noteq> UNIV"
+ using \<open>T \<noteq> {}\<close> by blast
+ have "C \<noteq> C'"
+ proof
+ assume "C = C'"
+ with that have "frontier C' \<subseteq> S \<inter> T"
+ by simp
+ also have "... = {}"
+ using \<open>S \<inter> T = {}\<close> by blast
+ finally have "C' = {} \<or> C' = UNIV"
+ using frontier_eq_empty by auto
+ then show False
+ using \<open>C = C'\<close> NUN that by (force simp: dest: in_components_nonempty in_components_subset)
+ qed
+ with that show ?thesis
+ by (simp add: components_nonoverlap [of _ "-(S \<union> T)"])
+ qed
+ then show ?thesis
+ by blast
+ qed
+ ultimately show "?S \<inter> ?T = {}"
+ using ST by blast
+ show "?S \<noteq> {}" "?T \<noteq> {}"
+ using \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> by blast+
+ qed
+ then show False
+ 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)
+qed
+
+
+lemma separation_by_component_open:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "open S" and non: "\<not> connected(- S)"
+ obtains C where "C \<in> components S" "\<not> connected(- C)"
+proof -
+ obtain T U
+ where "closed T" "closed U" and TU: "T \<union> U = - S" "T \<inter> U = {}" "T \<noteq> {}" "U \<noteq> {}"
+ using assms by (auto simp: connected_closed_set closed_def)
+ then obtain C where C: "C \<in> components(-(T \<union> U))" "C \<noteq> {}"
+ and "frontier C \<inter> T \<noteq> {}" "frontier C \<inter> U \<noteq> {}"
+ using separation_by_component_open_aux [OF \<open>closed T\<close> \<open>closed U\<close> \<open>T \<inter> U = {}\<close>] by force
+ show "thesis"
+ proof
+ show "C \<in> components S"
+ using C(1) TU(1) by auto
+ show "\<not> connected (- C)"
+ proof
+ assume "connected (- C)"
+ then have "connected (frontier C)"
+ using connected_frontier_simple [of C] \<open>C \<in> components S\<close> in_components_connected by blast
+ then show False
+ unfolding connected_closed
+ 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)
+ qed
+ qed
+qed
+
+lemma separation_by_Un_open:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "open S" "open T" "S \<inter> T = {}" and cS: "connected(-S)" and cT: "connected(-T)"
+ shows "connected(- (S \<union> T))"
+ using assms unicoherent_UNIV unfolding unicoherent_def by force
+
+
+lemma nonseparation_by_component_eq:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "open S \<or> closed S"
+ shows "((\<forall>C \<in> components S. connected(-C)) \<longleftrightarrow> connected(- S))" (is "?lhs = ?rhs")
+proof
+ assume ?lhs with assms show ?rhs
+ by (meson separation_by_component_closed separation_by_component_open)
+next
+ assume ?rhs with assms show ?lhs
+ using component_complement_connected by force
+qed
+
+
+text\<open>Another interesting equivalent of an inessential mapping into C-{0}\<close>
+proposition inessential_eq_extensible:
+ fixes f :: "'a::euclidean_space \<Rightarrow> complex"
+ assumes "closed S"
+ shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
+ (\<exists>g. continuous_on UNIV g \<and> (\<forall>x \<in> S. g x = f x) \<and> (\<forall>x. g x \<noteq> 0))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then obtain a where a: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)" ..
+ show ?rhs
+ proof (cases "S = {}")
+ case True
+ with a show ?thesis
+ using continuous_on_const by force
+ next
+ case False
+ have anr: "ANR (-{0::complex})"
+ by (simp add: ANR_delete open_Compl open_imp_ANR)
+ obtain g where contg: "continuous_on UNIV g" and gim: "g ` UNIV \<subseteq> -{0}"
+ and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ proof (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ homotopic_with_symD [OF a]])
+ show "closedin (subtopology euclidean UNIV) S"
+ using assms by auto
+ show "range (\<lambda>t. a) \<subseteq> - {0}"
+ using a homotopic_with_imp_subset2 False by blast
+ qed (use anr that in \<open>force+\<close>)
+ then show ?thesis
+ by force
+ qed
+next
+ assume ?rhs
+ then obtain g where contg: "continuous_on UNIV g"
+ and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x" and non0: "\<And>x. g x \<noteq> 0"
+ by metis
+ obtain h k::"'a\<Rightarrow>'a" where hk: "homeomorphism (ball 0 1) UNIV h k"
+ using homeomorphic_ball01_UNIV homeomorphic_def by blast
+ then have "continuous_on (ball 0 1) (g \<circ> h)"
+ by (meson contg continuous_on_compose continuous_on_subset homeomorphism_cont1 top_greatest)
+ then obtain j where contj: "continuous_on (ball 0 1) j"
+ and j: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> exp(j z) = (g \<circ> h) z"
+ by (metis (mono_tags, hide_lams) continuous_logarithm_on_ball comp_apply non0)
+ have [simp]: "\<And>x. x \<in> S \<Longrightarrow> h (k x) = x"
+ using hk homeomorphism_apply2 by blast
+ have "\<exists>\<zeta>. continuous_on S \<zeta>\<and> (\<forall>x\<in>S. f x = exp (\<zeta> x))"
+ proof (intro exI conjI ballI)
+ show "continuous_on S (j \<circ> k)"
+ proof (rule continuous_on_compose)
+ show "continuous_on S k"
+ by (meson continuous_on_subset hk homeomorphism_cont2 top_greatest)
+ show "continuous_on (k ` S) j"
+ apply (rule continuous_on_subset [OF contj])
+ using homeomorphism_image2 [OF hk] continuous_on_subset [OF contj] by blast
+ qed
+ show "f x = exp ((j \<circ> k) x)" if "x \<in> S" for x
+ proof -
+ have "f x = (g \<circ> h) (k x)"
+ by (simp add: gf that)
+ also have "... = exp (j (k x))"
+ by (metis rangeI homeomorphism_image2 [OF hk] j)
+ finally show ?thesis by simp
+ qed
+ qed
+ then show ?lhs
+ by (simp add: inessential_eq_continuous_logarithm)
+qed
+
+lemma inessential_on_clopen_Union:
+ fixes \<F> :: "'a::euclidean_space set set"
+ assumes T: "path_connected T"
+ and "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
+ and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
+ and hom: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)"
+ obtains a where "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
+proof (cases "\<Union>\<F> = {}")
+ case True
+ with that show ?thesis
+ by force
+next
+ case False
+ then obtain C where "C \<in> \<F>" "C \<noteq> {}"
+ by blast
+ then obtain a where clo: "closedin (subtopology euclidean (\<Union>\<F>)) C"
+ and ope: "openin (subtopology euclidean (\<Union>\<F>)) C"
+ and "homotopic_with (\<lambda>x. True) C T f (\<lambda>x. a)"
+ using assms by blast
+ with \<open>C \<noteq> {}\<close> have "f ` C \<subseteq> T" "a \<in> T"
+ using homotopic_with_imp_subset1 homotopic_with_imp_subset2 by blast+
+ have "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
+ proof (rule homotopic_on_clopen_Union)
+ show "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
+ "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
+ by (simp_all add: assms)
+ show "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)" if "S \<in> \<F>" for S
+ proof (cases "S = {}")
+ case True
+ then show ?thesis
+ by auto
+ next
+ case False
+ then obtain b where "b \<in> S"
+ by blast
+ obtain c where c: "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)"
+ using \<open>S \<in> \<F>\<close> hom by blast
+ then have "c \<in> T"
+ using \<open>b \<in> S\<close> homotopic_with_imp_subset2 by blast
+ then have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. c)"
+ using T \<open>a \<in> T\<close> homotopic_constant_maps path_connected_component by blast
+ then show ?thesis
+ using c homotopic_with_symD homotopic_with_trans by blast
+ qed
+ qed
+ then show ?thesis ..
+qed
+
+lemma Janiszewski_dual:
+ fixes S :: "complex set"
+ assumes
+ "compact S" "compact T" "connected S" "connected T" "connected(- (S \<union> T))"
+ shows "connected(S \<inter> T)"
+proof -
+ have ST: "compact (S \<union> T)"
+ by (simp add: assms compact_Un)
+ with Borsukian_imp_unicoherent [of "S \<union> T"] ST assms
+ show ?thesis
+ by (auto simp: closed_subset compact_imp_closed Borsukian_separation_compact unicoherent_def)
+qed
+
end
diff -r d0f12783cd80 -r 04678058308f src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy Sun Oct 29 19:39:03 2017 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Mon Oct 30 16:02:59 2017 +0000
@@ -6969,7 +6969,7 @@
shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}"
apply (rule iffI)
using homotopy_eqv_def apply fastforce
-by (simp add: homotopy_eqv_contractible_sets contractible_empty)
+by (simp add: homotopy_eqv_contractible_sets)
lemma homotopy_eqv_empty2 [simp]:
fixes S :: "'a::real_normed_vector set"
diff -r d0f12783cd80 -r 04678058308f src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Oct 29 19:39:03 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Oct 30 16:02:59 2017 +0000
@@ -2501,6 +2501,29 @@
lemma frontier_closures: "frontier S = closure S \<inter> closure (- S)"
by (auto simp: frontier_def interior_closure)
+lemma frontier_Int: "frontier(S \<inter> T) = closure(S \<inter> T) \<inter> (frontier S \<union> frontier T)"
+proof -
+ have "closure (S \<inter> T) \<subseteq> closure S" "closure (S \<inter> T) \<subseteq> closure T"
+ by (simp_all add: closure_mono)
+ then show ?thesis
+ by (auto simp: frontier_closures)
+qed
+
+lemma frontier_Int_subset: "frontier(S \<inter> T) \<subseteq> frontier S \<union> frontier T"
+ by (auto simp: frontier_Int)
+
+lemma frontier_Int_closed:
+ assumes "closed S" "closed T"
+ shows "frontier(S \<inter> T) = (frontier S \<inter> T) \<union> (S \<inter> frontier T)"
+proof -
+ have "closure (S \<inter> T) = T \<inter> S"
+ using assms by (simp add: Int_commute closed_Int)
+ moreover have "T \<inter> (closure S \<inter> closure (- S)) = frontier S \<inter> T"
+ by (simp add: Int_commute frontier_closures)
+ ultimately show ?thesis
+ by (simp add: Int_Un_distrib Int_assoc Int_left_commute assms frontier_closures)
+qed
+
lemma frontier_straddle:
fixes a :: "'a::metric_space"
shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"
@@ -2528,6 +2551,9 @@
lemma frontier_complement [simp]: "frontier (- S) = frontier S"
by (auto simp: frontier_def closure_complement interior_complement)
+lemma frontier_Un_subset: "frontier(S \<union> T) \<subseteq> frontier S \<union> frontier T"
+ by (metis compl_sup frontier_Int_subset frontier_complement)
+
lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
using frontier_complement frontier_subset_eq[of "- S"]
unfolding open_closed by auto